Dedication

de Philip, para Wanda

amor da minha vida

knock knock knock

…

Preface

The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that a certain kind of formal structure may be read in two ways: either as a proposition in logic or as a type in computing. Further, a related structure may be read as either the proof of the proposition or as a programme of the corresponding type. Further still, simplification of proofs corresponds to evaluation of programs.

Accordingly, the title of this book also has two readings. It may be parsed as “(Programming Language) Foundations in Agda” or “Programming (Language Foundations) in Agda” — the specifications we will write in the proof assistant Agda both describe programming languages and are themselves programmes.

The book is aimed at students in the last year of an undergraduate honours programme or the first year of a master or doctorate degree. It aims to teach the fundamentals of operational semantics of programming languages, with simply-typed lambda calculus as the central example. The textbook is written as a literate script in Agda. The hope is that using a proof assistant will make the development more concrete and accessible to students, and give them rapid feedback to find and correct misapprehensions.

The book is broken into two parts. The first part, Logical Foundations, develops the needed formalisms. The second part, Programming Language Foundations, introduces basic methods of operational semantics.

Personal remarks

Since 2013, I have taught a course on Types and Semantics for Programming Languages to fourth-year undergraduates and masters students at the University of Edinburgh. An earlier version of that course was based on Benjamin Pierce’s excellentTAPL. My version was based of Pierce’s subsequent textbook,Software Foundations, written in collaboration with others and based on Coq. I am convinced of Pierce’s claim that basing a course around a proof assistant aids learning, as summarised in his ICFP Keynote,Lambda, The Ultimate TA.

However, after five years of experience, I have come to the conclusion that Coq is not the best vehicle. Too much of the course needs to focus on learning tactics for proof derivation, to the cost of learning the fundamentals of programming language theory. Every concept has to be learned twice: e.g., both the product data type, and the corresponding tactics for introduction and elimination of conjunctions. The rules Coq applies to generate induction hypotheses can sometimes seem mysterious. While thenotationconstruct permits pleasingly flexible syntax, it can be confusing that the same concept must always be given two names, e.g., bothsubst N x MandN [x := M]. Names of tactics are sometimes short and sometimes long; naming conventions in the standard library can be wildly inconsistent.Propositions as typesas a foundation of proof is present but hidden.

I found myself keen to recast the course in Agda. In Agda, there is no longer any need to learn about tactics: there is just dependently-typed programming, plain and simple. Introduction is always by a constructor, elimination is always by pattern matching. Induction is no longer a mysterious separate concept, but corresponds to the familiar notion of recursion. Mixfix syntax is flexible while using just one name for each concept, e.g., substitution is_[_:=_]. The standard library is not perfect, but there is a fair attempt at consistency.Propositions as typesas a foundation of proof is on proud display.

Alas, there is no textbook for programming language theory in Agda. Stump’sVerified Functional Programming in Agdacovers related ground, but focusses more on programming with dependent types than on the theory of programming languages.

The original goal was to simply adaptSoftware Foundations, maintaining the same text but transposing the code from Coq to Agda. But it quickly became clear to me that after five years in the classroom I had my own ideas about how to present the material. They say you should never write a book unless you cannotnotwrite the book, and I soon found that this was a book I could not not write.

I am fortunate that my student,Wen Kokke, was keen to help. She guided me as a newbie to Agda and provided an infrastructure that is easy to use and produces pages that are a pleasure to view.

Most of the text was written during a sabbatical in the first half of 2018.

— Philip Wadler, Rio de Janeiro, January–June 2018

A word on the exercises

Exercises labelled “(recommended)” are the ones students are required to do in the class taught at Edinburgh from this textbook.

Exercises labelled “(stretch)” are there to provide an extra challenge. Few students do all of these, but most attempt at least a few.

Exercises labelled “(practice)” are included for those who want extra practice.

You may need to import library functions required for the solution.

Please do not post answers to the exercises in a public place.

There is a private repository of answers to selected questions on github. Please contact Philip Wadler if you would like to access it.

Getting Started

Installing Agda and PLFA

You can read PLFAonlinewithout installing anything. However, if you wish to interact with the code or complete the exercises, you need several things:

• On macOS:The XCode Command Line Tools
• Git
• GHC and Cabal
• Agda
• Agda standard library
• PLFA

PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems.

There are several versions of Agda and its standard library online. If you are using a package manager, like Homebrew or Debian apt, the version of Agda available there may be out of date. Furthermore, Agda is under active development, so if you install the development version from the GitHub, you might find the developers have introduced changes which break the code here. Therefore, it’s important to have the specific versions of Agda and the standard library shown above.

On macOS: Install the XCode Command Line Tools

On macOS, you’ll need to installThe XCode Command Line Tools. For most versions of macOS, you can install these by running the following command:

xcode-select --install

Install Git

You can check whether you have Git by running the following command:

git --version

If you do not have Git, seethe Git downloads page.

Install GHC and Cabal

Agda is written in Haskell, so to install it we’ll need theGlorious Haskell Compilerversion 8.10.7 and its package managerCabal. We recommend installing both of these usingghcup.

Install Agda

The easiest way to install Agda is using Cabal. PLFA uses Agda version 2.6.2.2. Run the following command:

cabal update
cabal install Agda-2.6.2.2

This step will take a long time and a lot of memory to complete.

For further information, see theAgda installation instructions.

If you’d like, you cantest to see if you’ve installed Agda correctly.

Install PLFA and the Agda standard library

We recommend installing PLFA from Github into your home directory, by running the following command:

git clone --depth 1 --recurse-submodules --shallow-submodules https://github.com/plfa/plfa.github.io plfa

PLFA ships with the required version of the Agda standard library, so if you cloned with the--recurse-submodulesflag, you’ve already got it, in thestandard-librarydirectory!

Finally, we need to let Agda know where to find the Agda standard library and PLFA. Two configuration files are required, one which lists paths to the libraries and one which specifies which libraries to load by default.

On macOS and Unix, if PLFA is installed in your home directory and you have no existing library configuration files you wish to preserve, run the following commands:

mkdir -p ~/.agda
cp ~/plfa/data/dotagda/* ~/.agda

This provides access to both the Agda standard library and to PLFA as an Agda library.

Otherwise, you will need to edit the appropriate files. Both configuration files are located in the directoryAGDA_DIR. On UNIX and macOS,AGDA_DIRdefaults to~/.agda. On Windows,AGDA_DIRusually defaults to%AppData%\agda, where%AppData%usually defaults toC:\Users\USERNAME\AppData\Roaming.

• If theAGDA_DIRdirectory does not already exist, create it.
• InAGDA_DIR, create a plain-text file calledlibrariescontainingAGDA_STDLIB/standard-library.agda-lib, whereAGDA_STDLIBis the path to where the Agda standard library is located (e.g.,~/plfa/standard-library/). This lets Agda know that an Agda library calledstandard-libraryis available.
• InAGDA_DIR, create a plain-text file calleddefaultscontainingjustthe linestandard-library.
• If you want to complete the exercises or to import modules from the book, you will also need to provide access to PLFA as an Agda library. To do so, letPLFAb the path to the root directory for PLFA. AddPLFA/src/plfa.agda-libtoAGDA_DIR/librariesand addplfatoAGDA_DIR/defaults, each on a line of their own.

More information about placing the standard libraries is available fromthe Library Management pageof the Agda documentation.

Setting up an editor for Agda

Emacs

The recommended editor for Agda is Emacs. To install Emacs:

• On UNIX, the version of Emacs in your repository is probably fine as long as it is fairly recent. There are also links to the most recent release on theGNU Emacs downloads page.

• On MacOS,Aquamacsis probably the preferred version of Emacs, but GNU Emacs can also be installed via Homebrew or MacPorts. See theGNU Emacs downloads pagefor instructions.

• On Windows. See theGNU Emacs downloads pagefor instructions.

Make sure that you are able to open, edit, and save text files with your installation. Thetour of Emacspage on the GNU Emacs site describes how to access the tutorial within your Emacs installation.

Agda ships with the editor support for Emacs built-in, so if you’ve installed Agda, all you have to do to configure Emacs is run:

agda-mode setup
agda-mode compile

If you are already an Emacs user and have customized your setup, you may want to note the configuration which thesetupappends to your.emacsfile, and integrate it with your own preferred setup.

Check ifagda-modewas installed correctly

Open thenats.agdafile you created earlier, and load and type-check the file by typingC-c C-l.

Auto-loadingagda-modein Emacs

Since version 2.6.0, Agda has had support for literate editing with Markdown, using the.lagda.mdextension. One issue is that Emacs will default to Markdown editing mode for files with a.mdsuffix. In order to haveagda-modeautomatically loaded whenever you open a file ending with.agdaor.lagda.md, add the following line to your Emacs configuration file:

;; auto-load agda-mode for .agda and .lagda.md
(setq auto-mode-alist
   (append
     '(("\\.agda\\'" . agda2-mode)
       ("\\.lagda.md\\'" . agda2-mode))
     auto-mode-alist))

If you already have settings which change yourauto-mode-alistin your configuration, put theseafterthe ones you already have or combine them if you are comfortable with Emacs Lisp. The configuration file for Emacs is normally located inHOME/.emacsorHOME/.emacs.d/init.el, but Aquamacs users might need to move their startup settings to the “Preferences.el” file inHOME/Library/Preferences/Aquamacs Emacs/Preferences. For Windows, seethe GNU Emacs documentationfor a description of where the Emacs configuration is located.

Optional: using the mononoki font with Emacs

Agda uses Unicode characters for many key symbols, and it is important that the font which you use to view and edit Agda programs shows these symbols correctly. The most important part is that the font you use has good Unicode support, so while we recommendmononoki, fonts such asSource Code Pro,DejaVu Sans Mono, andFreeMonoare all good alternatives.

You can download and install mononoki directly fromGitHub. For most systems, installing a font is merely a matter of clicking the downloaded.otfor.ttffile. If your package manager offers a package for mononoki, that might be easier. For instance, Homebrew on macOS offers thefont-mononokipackage in thecask-fontscask, and APT on Debian offers thefonts-mononokipackage. To configure Emacs to use mononoki as its default font, add the following to the end of your Emacs configuration file:

;; default to mononoki
(set-face-attribute 'default nil
                    :family "mononoki"
                    :height 120
                    :weight 'normal
                    :width  'normal)

Usingagda-modein Emacs

To load and type-check the file, useC-c C-l.

Agda is edited interactively, using“holes”, which are bits of the program that are not yet filled in. If you use a question mark as an expression, and load the buffer usingC-c C-l, Agda replaces the question mark with a hole. There are several things you can to while the cursor is in a hole:

• C-c C-c:case split (asks for variable name)
• C-c C-space: fill in hole
• C-c C-r:refine with constructor
• C-c C-a:automatically fill in hole
• C-c C-,: goal type and context
• C-c C-.: goal type, context, and inferred type

Seethe emacs-mode docsfor more details.

If you want to see messages beside rather than below your Agda code, you can do the following:

• Open your Agda file, and load it usingC-c C-l;
• typeC-x 1to get only your Agda file showing;
• typeC-x 3to split the window horizontally;
• move your cursor to the right-hand half of your frame;
• typeC-x band switch to the buffer called “Agda information”.

Now, error messages from Agda will appear next to your file, rather than squished beneath it.

Entering Unicode characters in Emacs withagda-mode

When you write Agda code, you will need to insert characters which are not found on standard keyboards. Emacs “agda-mode” makes it easier to do this by defining character translations: when you enter certain sequences of ordinary characters (the kind you find on any keyboard), Emacs will replace them in your Agda file with the corresponding special character.

For example, we can add a comment line to one of the.agdatest files. Let’s say we want to add a comment line that reads:

{- I am excited to type ∀ and → and ≤ and ≡ !! -}

The first few characters are ordinary, so we would just type them as usual…

{- I am excited to type

But after that last space, we do not find ∀ on the keyboard. The code for this character is the four characters\all, so we type those four characters, and when we finish, Emacs will replace them with what we want…

{- I am excited to type ∀

We can continue with the codes for the other characters. Sometimes the characters will change as we type them, because a prefix of our character’s code is the code of another character. This happens with the arrow, whose code is\->. After typing\-we see…

{- I am excited to type ∀ and

…because the code\-corresponds to a hyphen of a certain width. When we add the>, the­becomes→! The code for≤is\<=, and the code for≡is\==.

{- I am excited to type ∀ and → and ≤ and ≡

Finally the last few characters are ordinary again…

{- I am excited to type ∀ and → and ≤ and ≡ !! -}

If you’re having trouble typing the Unicode characters into Emacs, the end of each chapter should provide a list of the Unicode characters introduced in that chapter.

Emacs withagda-modeoffers a number of useful commands, and two of them are especially useful when it comes to working with Unicode characters. For a full list of supported characters, useagda-input-show-translationswith:

M-x agda-input-show-translations

All the supported characters inagda-modeare shown.

If you want to know how you input a specific Unicode character in agda file, move the cursor onto the character and type the following command:

M-x quail-show-key

You’ll see the key sequence of the character in mini buffer.

Spacemacs

Spacemacsis a “community-driven Emacs distribution” with native support for both Emacs and Vim editing styles. It comes withintegration foragda-modeout of the box. All that is required is that you turn it on.

Visual Studio Code

Visual Studio Codeis a free source code editor developed by Microsoft. There isa plugin for Agda supportavailable on the Visual Studio Marketplace.

Atom

Atomis a free source code editor developed by GitHub. There isa plugin for Agda supportavailable on the Atom package manager.

Naturals: Natural numbers

module plfa.part1.Naturals where

The night sky holds more stars than I can count, though fewer than five thousand are visible to the naked eye. The observable universe contains about seventy sextillion stars.

But the number of stars is finite, while natural numbers are infinite. Count all the stars, and you will still have as many natural numbers left over as you started with.

The naturals are an inductive datatype

Everyone is familiar with the natural numbers

0
1
2
3
...

and so on. We writeℕfor thetypeof natural numbers, and say that0,1,2,3, and so on arevaluesof typeℕ, indicated by writing0 : ℕ,1 : ℕ,2 : ℕ,3 : ℕ, and so on.

The set of natural numbers is infinite, yet we can write down its definition in just a few lines. Here is the definition as a pair of inference rules:

--------
zero : ℕ

m : ℕ
---------
suc m : ℕ

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

Hereℕis the name of thedatatypewe are defining, andzeroandsuc(short forsuccessor) are theconstructorsof the datatype.

Both definitions above tell us the same two things:

• Base case:zerois a natural number.
• Inductive case: ifmis a natural number, thensuc mis also a natural number.

Further, these two rules give theonlyways of creating natural numbers. Hence, the possible natural numbers are:

zero
suc zero
suc (suc zero)
suc (suc (suc zero))
...

We write0as shorthand forzero; and1is shorthand forsuc zero, the successor of zero, that is, the natural that comes after zero; and2is shorthand forsuc (suc zero), which is the same assuc 1, the successor of one; and3is shorthand for the successor of two; and so on.

Exerciseseven(practice)

Write out7in longhand.

-- Your code goes here

You will need to give both a type signature and definition for the variableseven. TypeC-c C-lin Emacs to instruct Agda to re-load.

Unpacking the inference rules

Let’s unpack the inference rules. Each inference rule consists of zero or morejudgmentswritten above a horizontal line, called thehypotheses, and a single judgment written below, called theconclusion. The first rule is the base case. It has no hypotheses, and the conclusion asserts thatzerois a natural. The second rule is the inductive case. It has one hypothesis, which assumes thatmis a natural, and the conclusion asserts thatsuc mis also a natural.

Unpacking the Agda definition

Let’s unpack the Agda definition. The keyworddatatells us this is an inductive definition, that is, that we are defining a new datatype with constructors. The phrase

ℕ : Set

tells us thatℕis the name of the new datatype, and that it is aSet, which is the way in Agda of saying that it is a type. The keywordwhereseparates the declaration of the datatype from the declaration of its constructors. Each constructor is declared on a separate line, which is indented to indicate that it belongs to the correspondingdatadeclaration. The lines

zero : ℕ
suc  : ℕ → ℕ

givesignaturesspecifying the types of the constructorszeroandsuc. They tell us thatzerois a natural number and thatsuctakes a natural number as an argument and returns a natural number.

You may have noticed thatℕand→don’t appear on your keyboard. They are symbols inunicode. At the end of each chapter is a list of all unicode symbols introduced in the chapter, including instructions on how to type them in the Emacs text editor. Heretyperefers to typing with fingers as opposed to data types!

The story of creation

Let’s look again at the rules that define the natural numbers:

• Base case:zerois a natural number.
• Inductive case: ifmis a natural number, thensuc mis also a natural number.

Hold on! The second line defines natural numbers in terms of natural numbers. How can that possibly be allowed? Isn’t this as useless a definition as “Brexit means Brexit”?

In fact, it is possible to assign our definition a meaning without resorting to unpermitted circularities. Furthermore, we can do so while only working withfinitesets and never referring to theinfiniteset of natural numbers.

We will think of it as a creation story. To start with, we know about no natural numbers at all:

-- In the beginning, there are no natural numbers.

Now, we apply the rules to all the natural numbers we know about. The base case tells us thatzerois a natural number, so we add it to the set of known natural numbers. The inductive case tells us that ifmis a natural number (on the day before today) thensuc mis also a natural number (today). We didn’t know about any natural numbers before today, so the inductive case doesn’t apply:

-- On the first day, there is one natural number.
zero : ℕ

Then we repeat the process. On the next day we know about all the numbers from the day before, plus any numbers added by the rules. The base case tells us thatzerois a natural number, but we already knew that. But now the inductive case tells us that sincezerowas a natural number yesterday, thensuc zerois a natural number today:

-- On the second day, there are two natural numbers.
zero : ℕ
suc zero : ℕ

And we repeat the process again. Now the inductive case tells us that sincezeroandsuc zeroare both natural numbers, thensuc zeroandsuc (suc zero)are natural numbers. We already knew about the first of these, but the second is new:

-- On the third day, there are three natural numbers.
zero : ℕ
suc zero : ℕ
suc (suc zero) : ℕ

You’ve got the hang of it by now:

-- On the fourth day, there are four natural numbers.
zero : ℕ
suc zero : ℕ
suc (suc zero) : ℕ
suc (suc (suc zero)) : ℕ

The process continues. On then’th day there will bendistinct natural numbers. Every natural number will appear on some given day. In particular, the numbernfirst appears on dayn+1. And we never actually define the set of numbers in terms of itself. Instead, we define the set of numbers on dayn+1in terms of the set of numbers on dayn.

A process like this one is calledinductive. We start with nothing, and build up a potentially infinite set by applying rules that convert one finite set into another finite set.

The rule defining zero is called abase case, because it introduces a natural number even when we know no other natural numbers. The rule defining successor is called aninductive case, because it introduces more natural numbers once we already know some. Note the crucial role of the base case. If we only had inductive rules, then we would have no numbers in the beginning, and still no numbers on the second day, and on the third, and so on. An inductive definition lacking a base case is useless, as in the phrase “Brexit means Brexit”.

Philosophy and history

A philosopher might observe that our reference to the first day, second day, and so on, implicitly involves an understanding of natural numbers. In this sense, our definition might indeed be regarded as in some sense circular, but we need not let this disturb us. Everyone possesses a good informal understanding of the natural numbers, which we may take as a foundation for their formal description.

While the natural numbers have been understood for as long as people can count, the inductive definition of the natural numbers is relatively recent. It can be traced back to Richard Dedekind’s paper “Was sind und was sollen die Zahlen?” (What are and what should be the numbers?), published in 1888, and Giuseppe Peano’s book “Arithmetices principia, nova methodo exposita” (The principles of arithmetic presented by a new method), published the following year.

A pragma

In Agda, any text following--or enclosed between{-and-}is considered acomment. Comments have no effect on the code, with the exception of one special kind of comment, called apragma, which is enclosed between{-#and#-}.

{-# BUILTIN NATURAL ℕ #-}

tells Agda thatℕcorresponds to the natural numbers, and hence one is permitted to type0as shorthand forzero,1as shorthand forsuc zero,2as shorthand forsuc (suc zero), and so on. The pragma must be given a previously declared type (in this caseℕ) with precisely two constructors, one with no arguments (in this casezero), and one with a single argument of the given type (in this casesuc).

As well as enabling the above shorthand, the pragma also enables a more efficient internal representation of naturals using the Haskell type for arbitrary-precision integers. Representing the naturalnwithzeroandsucrequires space proportional ton, whereas representing it as an arbitrary-precision integer in Haskell only requires space proportional to the logarithm ofn.

Imports

Shortly we will want to write some equations that hold between terms involving natural numbers. To support doing so, we import the definition of equality and notations for reasoning about it from the Agda standard library:

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

The first line brings the standard library module that defines equality into scope and gives it the nameEq. The second line opens that module, that is, adds all the names specified in theusingclause into the current scope. In this case the names added are_≡_, the equality operator, andrefl, the name for evidence that two terms are equal. The third line takes a module that specifies operators to support reasoning about equivalence, and adds all the names specified in theusingclause into the current scope. In this case, the names added arebegin_,_≡⟨⟩_, and_∎. We will see how these are used below. We take these as givens for now, but will see how they are defined in ChapterEquality.

Agda uses underbars to indicate where terms appear in infix or mixfix operators. Thus,_≡_and_≡⟨⟩_are infix (each operator is written between two terms), whilebegin_is prefix (it is written before a term), and_∎is postfix (it is written after a term).

Parentheses and semicolons are among the few characters that cannot appear in names, so we do not need extra spaces in theusinglist.

Operations on naturals are recursive functions

Now that we have the natural numbers, what can we do with them? For instance, can we define arithmetic operations such as addition and multiplication?

As a child I spent much time memorising tables of addition and multiplication. At first the rules seemed tricky and I would often make mistakes. It came as a shock to me to discoverrecursion, a simple technique by which every one of the infinite possible instances of addition and multiplication can be specified in just a couple of lines.

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

Let’s unpack this definition. Addition is an infix operator. It is written with underbars where the arguments go, hence its name is_+_. The first line is a signature specifying the type of the operator. The typeℕ → ℕ → ℕ, indicates that addition accepts two naturals and returns a natural. Infix notation is just a shorthand for application; the termsm + nand_+_ m nare equivalent.

The definition has a base case and an inductive case, corresponding to those for the natural numbers. The base case says that adding zero to a number,zero + n, returns that number,n. The inductive case says that adding the successor of a number to another number,(suc m) + n, returns the successor of adding the two numbers,suc (m + n). We say we usepattern matchingwhen constructors appear on the left-hand side of an equation.

If we writezeroas0andsuc mas1 + m, the definition turns into two familiar equations:

 0       + n  ≡  n
 (1 + m) + n  ≡  1 + (m + n)

The first follows because zero is an identity for addition, and the second because addition is associative. In its most general form, associativity is written

 (m + n) + p  ≡  m + (n + p)

meaning that the location of parentheses is irrelevant. We get the second equation from the third by takingmto be1,nto bem, andpto ben. We write=for definitions, while we write≡for assertions that two already defined things are the same.

The definition isrecursive, in that the last line defines addition in terms of addition. As with the inductive definition of the naturals, the apparent circularity is not a problem. It works because addition of larger numbers is defined in terms of addition of smaller numbers. Such a definition is calledwell founded.

_ :  +  ≡ 
_ =
  begin
     + 
  ≡⟨⟩    -- is shorthand for
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩    -- inductive case
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩    -- inductive case
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩    -- base case
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩    -- is longhand for
    
  ∎

_ :  +  ≡ 
_ =
  begin
     + 
  ≡⟨⟩
    suc ( + )
  ≡⟨⟩
    suc (suc ( + ))
  ≡⟨⟩
    suc (suc )
  ≡⟨⟩
    
  ∎

The first line matches the inductive case by takingm = 1andn = 3, the second line matches the inductive case by takingm = 0andn = 3, and the third line matches the base case by takingn = 3.

Both derivations consist of a signature (written with a colon,:), giving a type, and a binding (written with an equal sign,=), giving a term of the given type. Here we use the dummy name_. The dummy name can be reused, and is convenient for examples. Names other than_must be used only once in a module.

Here the type is2 + 3 ≡ 5and the term providesevidencefor the corresponding equation, here written in tabular form as a chain of equations. The chain starts withbeginand finishes with∎(pronounced “qed” or “tombstone”, the latter from its appearance), and consists of a series of terms separated by≡⟨⟩.

_ :  +  ≡ 
_ = refl

Agda knows how to compute the value of2 + 3, and so can immediately check it is the same as5. A binary relation is said to bereflexiveif every value relates to itself. Evidence that a value is equal to itself is writtenrefl.

In the chains of equations, all Agda checks is that each term simplifies to the same value. If we jumble the equations, omit lines, or add extraneous lines it will still be accepted. It’s up to us to write the equations in an order that makes sense to the reader.

Here2 + 3 ≡ 5is a type, and the chains of equations (and alsorefl) are terms of the given type; alternatively, one can think of each term asevidencefor the assertion2 + 3 ≡ 5. This duality of interpretation—of a type as a proposition, and of a term as evidence—is central to how we formalise concepts in Agda, and will be a running theme throughout this book.

Note that when we use the wordevidenceit is nothing equivocal. It is not like testimony in a court which must be weighed to determine whether the witness is trustworthy. Rather, it is ironclad. The other word for evidence, which we will use interchangeably, isproof.

Exercise+-example(practice)

Compute3 + 4, writing out your reasoning as a chain of equations, using the equations for+.

-- Your code goes here

Multiplication

_*_ : ℕ → ℕ → ℕ
zero    * n  =  zero
(suc m) * n  =  n + (m * n)

Computingm * nreturns the sum ofmcopies ofn.

Again, rewriting turns the definition into two familiar equations:

0       * n  ≡  0
(1 + m) * n  ≡  n + (m * n)

The first follows because zero times anything is zero, and the second follows because multiplication distributes over addition. In its most general form, distribution of multiplication over addition is written

(m + n) * p  ≡  (m * p) + (n * p)

We get the second equation from the third by takingmto be1,nto bem, andpto ben, and then using the fact that one is an identity for multiplication, so1 * n ≡ n.

Again, the definition is well founded in that multiplication of larger numbers is defined in terms of multiplication of smaller numbers.

_ =
  begin
     * 
  ≡⟨⟩    -- inductive case
     + ( * )
  ≡⟨⟩    -- inductive case
     + ( + ( * ))
  ≡⟨⟩    -- base case
     + ( + )
  ≡⟨⟩    -- simplify
    
  ∎

The first line matches the inductive case by takingm = 1andn = 3, the second line matches the inductive case by takingm = 0andn = 3, and the third line matches the base case by takingn = 3. Here we have omitted the signature declaring_ : 2 * 3 ≡ 6, since it can easily be inferred from the corresponding term.

Exercise*-example(practice)

Compute3 * 4, writing out your reasoning as a chain of equations, using the equations for*. (You do not need to step through the evaluation of+.)

-- Your code goes here

Exercise_^_(recommended)

Define exponentiation, which is given by the following equations:

m ^ 0        =  1
m ^ (1 + n)  =  m * (m ^ n)

Check that3 ^ 4is81.

-- Your code goes here

Monus

We can also define subtraction. Since there are no negative natural numbers, if we subtract a larger number from a smaller number we will take the result to be zero. This adaption of subtraction to naturals is calledmonus(a twist onminus).

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

We can do a simple analysis to show that all the cases are covered.

• Consider the second argument.
  • If it iszero, then the first equation applies.
  • If it issuc n, then consider the first argument.
    • If it iszero, then the second equation applies.
    • If it issuc m, then the third equation applies.

Again, the recursive definition is well founded because monus on bigger numbers is defined in terms of monus on smaller numbers.

_ =
  begin
     ∸ 
  ≡⟨⟩
     ∸ 
  ≡⟨⟩
     ∸ 
  ≡⟨⟩
    
  ∎

_ =
  begin
     ∸ 
  ≡⟨⟩
     ∸ 
  ≡⟨⟩
     ∸ 
  ≡⟨⟩
    
  ∎

Exercise∸-example₁and∸-example₂(recommended)

Compute5 ∸ 3and3 ∸ 5, writing out your reasoning as a chain of equations.

-- Your code goes here

Precedence

We often useprecedenceto avoid writing too many parentheses. Applicationbinds more tightly than(orhas precedence over) any operator, and so we may writesuc m + nto mean(suc m) + n. As another example, we say that multiplication binds more tightly than addition, and so writen + m * nto meann + (m * n). We also sometimes say that additionassociates to the left, and so writem + n + pto mean(m + n) + p.

infixl   _+_  _∸_
infixl   _*_

This states operators_+_and_∸_have precedence level 6, and operator_*_has precedence level 7. Addition and monus bind less tightly than multiplication because they have lower precedence. Writinginfixlindicates that all three operators associate to the left. One can also writeinfixrto indicate that an operator associates to the right, or justinfixto indicate that parentheses are always required to disambiguate.

Currying

We have chosen to represent a function of two arguments in terms of a function of the first argument that returns a function of the second argument. This trick goes by the namecurrying.

Agda, like other functional languages such as Haskell and ML, is designed to make currying easy to use. Function arrows associate to the right and application associates to the left

ℕ → ℕ → ℕstands forℕ → (ℕ → ℕ)

and

_+_ 2 3stands for(_+_ 2) 3.

The term_+_ 2by itself stands for the function that adds two to its argument, hence applying it to three yields five.

Currying is named for Haskell Curry, after whom the programming language Haskell is also named. Curry’s work dates to the 1930’s. When I first learned about currying, I was told it was misattributed, since the same idea was previously proposed by Moses Schönfinkel in the 1920’s. I was told a joke: “It should be called schönfinkeling, but currying is tastier”. Only later did I learn that the explanation of the misattribution was itself a misattribution. The idea actually appears in theBegriffsschriftof Gottlob Frege, published in 1879.

The story of creation, revisited

Just as our inductive definition defines the naturals in terms of the naturals, so does our recursive definition define addition in terms of addition.

Again, it is possible to assign our definition a meaning without resorting to unpermitted circularities. We do so by reducing our definition to equivalent inference rules for judgments about equality:

n : ℕ
--------------
zero + n  =  n

m + n  =  p
---------------------
(suc m) + n  =  suc p

Here we assume we have already defined the infinite set of natural numbers, specifying the meaning of the judgmentn : ℕ. The first inference rule is the base case. It asserts that ifnis a natural number then adding zero to it givesn. The second inference rule is the inductive case. It asserts that if addingmandngivesp, then addingsuc mandngivessuc p.

Again we resort to a creation story, where this time we are concerned with judgments about addition:

-- In the beginning, we know nothing about addition.

Now, we apply the rules to all the judgment we know about. The base case tells us thatzero + n = nfor every naturaln, so we add all those equations. The inductive case tells us that ifm + n = p(on the day before today) thensuc m + n = suc p(today). We didn’t know any equations about addition before today, so that rule doesn’t give us any new equations:

-- On the first day, we know about addition of 0.
0 + 0 = 0     0 + 1 = 1    0 + 2 = 2     ...

Then we repeat the process, so on the next day we know about all the equations from the day before, plus any equations added by the rules. The base case tells us nothing new, but now the inductive case adds more equations:

-- On the second day, we know about addition of 0 and 1.
0 + 0 = 0     0 + 1 = 1     0 + 2 = 2     0 + 3 = 3     ...
1 + 0 = 1     1 + 1 = 2     1 + 2 = 3     1 + 3 = 4     ...

And we repeat the process again:

-- On the third day, we know about addition of 0, 1, and 2.
0 + 0 = 0     0 + 1 = 1     0 + 2 = 2     0 + 3 = 3     ...
1 + 0 = 1     1 + 1 = 2     1 + 2 = 3     1 + 3 = 4     ...
2 + 0 = 2     2 + 1 = 3     2 + 2 = 4     2 + 3 = 5     ...

You’ve got the hang of it by now:

-- On the fourth day, we know about addition of 0, 1, 2, and 3.
0 + 0 = 0     0 + 1 = 1     0 + 2 = 2     0 + 3 = 3     ...
1 + 0 = 1     1 + 1 = 2     1 + 2 = 3     1 + 3 = 4     ...
2 + 0 = 2     2 + 1 = 3     2 + 2 = 4     2 + 3 = 5     ...
3 + 0 = 3     3 + 1 = 4     3 + 2 = 5     3 + 3 = 6     ...

The process continues. On them’th day we will know all the equations where the first number is less thanm.

As we can see, the reasoning that justifies inductive and recursive definitions is quite similar. They might be considered two sides of the same coin.

The story of creation, finitely

The above story was told in a stratified way. First, we create the infinite set of naturals. We take that set as given when creating instances of addition, so even on day one we have an infinite set of instances.

Instead, we could choose to create both the naturals and the instances of addition at the same time. Then on any day there would be only a finite set of instances:

-- In the beginning, we know nothing.

Now, we apply the rules to all the judgment we know about. Only the base case for naturals applies:

-- On the first day, we know zero.
0 : ℕ

Again, we apply all the rules we know. This gives us a new natural, and our first equation about addition.

-- On the second day, we know one and all sums that yield zero.
0 : ℕ
1 : ℕ    0 + 0 = 0

Then we repeat the process. We get one more equation about addition from the base case, and also get an equation from the inductive case, applied to equation of the previous day:

-- On the third day, we know two and all sums that yield one.
0 : ℕ
1 : ℕ    0 + 0 = 0
2 : ℕ    0 + 1 = 1   1 + 0 = 1

You’ve got the hang of it by now:

-- On the fourth day, we know three and all sums that yield two.
0 : ℕ
1 : ℕ    0 + 0 = 0
2 : ℕ    0 + 1 = 1   1 + 0 = 1
3 : ℕ    0 + 2 = 2   1 + 1 = 2    2 + 0 = 2

On then’th day there will bendistinct natural numbers, andn × (n-1) / 2equations about addition. The numbernand all equations for addition of numbers less thannfirst appear by dayn+1. This gives an entirely finitist view of infinite sets of data and equations relating the data.

Writing definitions interactively

Agda is designed to be used with the Emacs text editor, and the two in combination provide features that help to create definitions and proofs interactively.

Begin by typing:

_+_ : ℕ → ℕ → ℕ
m + n = ?

The question mark indicates that you would like Agda to help with filling in that part of the code. If you typeC-c C-l(pressing the control key while hitting theckey followed by thelkey), which stands forload, the question mark will be replaced:

_+_ : ℕ → ℕ → ℕ
m + n = { }0

The empty braces are called ahole, and 0 is a number used for referring to the hole. The hole will display highlighted in green. Emacs will also create a window displaying the text

?0 : ℕ

to indicate that hole 0 is to be filled in with a term of typeℕ. TypingC-c C-f(forforward) will move you into the next hole.

We wish to define addition by recursion on the first argument. Move the cursor into the hole and typeC-c C-c(forcase). You will be given the prompt:

pattern variables to case (empty for split on result):

Typingmwill cause a split on that variable, resulting in an update to the code:

_+_ : ℕ → ℕ → ℕ
zero + n = { }0
suc m + n = { }1

There are now two holes, and the window at the bottom tells you the required type of each:

?0 : ℕ
?1 : ℕ

Going into hole 0 and typingC-c C-,will display information on the required type of the hole, and what free variables are available:

Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ

This strongly suggests filling the hole withn. After the hole is filled, you can typeC-c C-space, which will remove the hole:

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = { }1

Again, going into hole 1 and typingC-c C-,will display information on the required type of the hole, and what free variables are available:

Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ
m : ℕ

Going into the hole and typeC-c C-r(forrefine) will fill it in with a constructor (if there is a unique choice) or tell you what constructors you might use, if there is a choice. In this case, it displays the following:

Don't know which constructor to introduce of zero or suc

Filling the hole withsuc ?and typingC-c C-spaceresults in the following:

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc { }1

Going into the new hole and typingC-c C-,gives similar information to before:

Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ
m : ℕ

We can fill the hole withm + nand typeC-c C-spaceto complete the program:

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

Exploiting interaction to this degree is probably not helpful for a program this simple, but the same techniques can help with more complex programs. Even for a program this simple, usingC-c C-cto split cases can be helpful.

More pragmas

{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _∸_ #-}

tells Agda that these three operators correspond to the usual ones, and enables it to perform these computations using the corresponding Haskell operators on the arbitrary-precision integer type. Representing naturals withzeroandsucrequires time proportional tomto addmandn, whereas representing naturals as integers in Haskell requires time proportional to the larger of the logarithms ofmandn. Similarly, representing naturals withzeroandsucrequires time proportional to the product ofmandnto multiplymandn, whereas representing naturals as integers in Haskell requires time proportional to the sum of the logarithms ofmandn.

ExerciseBin(stretch)

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

For instance, the bitstring

1011

standing for the number eleven is encoded as

⟨⟩ I O I I

Representations are not unique due to leading zeros. Hence, eleven is also represented by001011, encoded as:

⟨⟩ O O I O I I

Define a function

inc : Bin → Bin

that converts a bitstring to the bitstring for the next higher number. For example, since1100encodes twelve, we should have:

inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O

Confirm that this gives the correct answer for the bitstrings encoding zero through four.

Using the above, define a pair of functions to convert between the two representations.

to   : ℕ → Bin
from : Bin → ℕ

For the former, choose the bitstring to have no leading zeros if it represents a positive natural, and represent zero by⟨⟩ O. Confirm that these both give the correct answer for zero through four.

-- Your code goes here

Standard library

At the end of each chapter, we will show where to find relevant definitions in the standard library. The naturals, constructors for them, and basic operators upon them, are defined in the standard library moduleData.Nat:

-- import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _∸_)

Normally, we will show an import as running code, so Agda will complain if we attempt to import a definition that is not available. This time, however, we have only shown the import as a comment. Both this chapter and the standard library invoke theNATURALpragma, the former onℕ, and the latter on the equivalent typeData.Nat.ℕ. Such a pragma can only be invoked once, as invoking it twice would raise confusion as to whether2is a value of typeℕor typeData.Nat.ℕ. Similar confusions arise if other pragmas are invoked twice. For this reason, we will usually avoid pragmas in future chapters. Information on pragmas can be found in theAgda documentation.

Unicode

This chapter uses the following unicode:

ℕ  U+2115  DOUBLE-STRUCK CAPITAL N (\bN)
→  U+2192  RIGHTWARDS ARROW (\to, \r, \->)
∸  U+2238  DOT MINUS (\.-)
≡  U+2261  IDENTICAL TO (\==)
⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)
⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
∎  U+220E  END OF PROOF (\qed)

Each line consists of the Unicode character (ℕ), the corresponding code point (U+2115), the name of the character (DOUBLE-STRUCK CAPITAL N), and the sequence to type into Emacs to generate the character (\bN).

The command\rgives access to a wide variety of rightward arrows. After typing\r, one can access the many available arrows by using the left, right, up, and down keys to navigate. The command remembers where you navigated to the last time, and starts with the same character next time. The command\lworks similarly for left arrows. In place of left, right, up, and down keys, one may also use control characters:

C-b  left (backward one character)
C-f  right (forward one character)
C-p  up (to the previous line)
C-n  down (to the next line)

We writeC-bto stand for control-b, and similarly. One can also navigate left and right by typing the digits that appear in the displayed list.

For a full list of supported characters, useagda-input-show-translationswith:

M-x agda-input-show-translations

All the characters supported byagda-modeare shown. We write M-x to stand for typingESCfollowed byx.

If you want to know how you input a specific Unicode character in an agda file, move the cursor onto the character and usequail-show-keywith:

M-x quail-show-key

You’ll see a key sequence of the character in mini buffer. If you runM-x quail-show-keyon say∸, you will see\.-for the character.

Induction: Proof by Induction

module plfa.part1.Induction where

Induction makes you feel guilty for getting something out of nothing … but it is one of the greatest ideas of civilization. – Herbert Wilf

Now that we’ve defined the naturals and operations upon them, our next step is to learn how to prove properties that they satisfy. As hinted by their name, properties ofinductive datatypesare proved byinduction.

Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

(Importingstep-≡defines_≡⟨_⟩_.)

Properties of operators

Operators pop up all the time, and mathematicians have agreed on names for some of the most common properties.

• Identity. Operator+has left identity0if0 + n ≡ n, and right identity0ifn + 0 ≡ n, for alln. A value that is both a left and right identity is just called an identity. Identity is also sometimes calledunit.

• Associativity. Operator+is associative if the location of parentheses does not matter:(m + n) + p ≡ m + (n + p), for allm,n, andp.

• Commutativity. Operator+is commutative if order of arguments does not matter:m + n ≡ n + m, for allmandn.

• Distributivity. Operator*distributes over operator+from the left ifm * (p + q) ≡ (m * p) + (m * q), for allm,p, andq, and from the right if(m + n) * p ≡ (m * p) + (n * p), for allm,n, andp.

Addition has identity0and multiplication has identity1; addition and multiplication are both associative and commutative; and multiplication distributes over addition.

If you ever bump into an operator at a party, you now know how to make small talk, by asking whether it has a unit and is associative or commutative. If you bump into two operators, you might ask them if one distributes over the other.

Less frivolously, if you ever bump into an operator while reading a technical paper, this gives you a way to orient yourself, by checking whether or not it has an identity, is associative or commutative, or distributes over another operator. A careful author will often call out these properties—or their lack—for instance by pointing out that a newly introduced operator is associative but not commutative.

Exerciseoperators(practice)

Give another example of a pair of operators that have an identity and are associative, commutative, and distribute over one another. (You do not have to prove these properties.)

Give an example of an operator that has an identity and is associative but is not commutative. (You do not have to prove these properties.)

Associativity

One property of addition is that it isassociative, that is, that the location of the parentheses does not matter:

(m + n) + p ≡ m + (n + p)

Herem,n, andpare variables that range over all natural numbers.

_ : ( + ) +  ≡  + ( + )
_ =
  begin
    ( + ) + 
  ≡⟨⟩
     + 
  ≡⟨⟩
    
  ≡⟨⟩
     + 
  ≡⟨⟩
     + ( + )
  ∎

Here we have displayed the computation as a chain of equations, one term to a line. It is often easiest to read such chains from the top down until one reaches the simplest term (in this case,12), and then from the bottom up until one reaches the same term.

The test reveals that associativity is perhaps not as obvious as first it appears. Why should7 + 5be the same as3 + 9? We might want to gather more evidence, testing the proposition by choosing other numbers. But—since there are an infinite number of naturals—testing can never be complete. Is there any way we can be sure that associativity holds forallthe natural numbers?

The answer is yes! We can prove a property holds for all naturals usingproof by induction.

Proof by induction

Recall the definition of natural numbers consists of abase casewhich tells us thatzerois a natural, and aninductive casewhich tells us that ifmis a natural thensuc mis also a natural.

Proof by induction follows the structure of this definition. To prove a property of natural numbers by induction, we need to prove two cases. First is thebase case, where we show the property holds forzero. Second is theinductive case, where we assume the property holds for an arbitrary naturalm(we call this theinductive hypothesis), and then show that the property must also hold forsuc m.

If we writeP mfor a property ofm, then what we need to demonstrate are the following two inference rules:

------
P zero

P m
---------
P (suc m)

Let’s unpack these rules. The first rule is the base case, and requires we show that propertyPholds forzero. The second rule is the inductive case, and requires we show that if we assume the inductive hypothesis—namely thatPholds form—then it follows thatPalso holds forsuc m.

Why does this work? Again, it can be explained by a creation story. To start with, we know no properties:

-- In the beginning, no properties are known.

Now, we apply the two rules to all the properties we know about. The base case tells us thatP zeroholds, so we add it to the set of known properties. The inductive case tells us that ifP mholds (on the day before today) thenP (suc m)also holds (today). We didn’t know about any properties before today, so the inductive case doesn’t apply:

-- On the first day, one property is known.
P zero

Then we repeat the process, so on the next day we know about all the properties from the day before, plus any properties added by the rules. The base case tells us thatP zeroholds, but we already knew that. But now the inductive case tells us that sinceP zeroheld yesterday, thenP (suc zero)holds today:

-- On the second day, two properties are known.
P zero
P (suc zero)

And we repeat the process again. Now the inductive case tells us that sinceP zeroandP (suc zero)both hold, thenP (suc zero)andP (suc (suc zero))also hold. We already knew about the first of these, but the second is new:

-- On the third day, three properties are known.
P zero
P (suc zero)
P (suc (suc zero))

You’ve got the hang of it by now:

-- On the fourth day, four properties are known.
P zero
P (suc zero)
P (suc (suc zero))
P (suc (suc (suc zero)))

The process continues. On then’th day there will bendistinct properties that hold. The property of every natural number will appear on some given day. In particular, the propertyP nfirst appears on dayn+1.

Our first proof: associativity

To prove associativity, we takeP mto be the property:

(m + n) + p ≡ m + (n + p)

Herenandpare arbitrary natural numbers, so if we can show the equation holds for allmit will also hold for allnandp. The appropriate instances of the inference rules are:

-------------------------------
(zero + n) + p ≡ zero + (n + p)

(m + n) + p ≡ m + (n + p)
---------------------------------
(suc m + n) + p ≡ suc m + (n + p)

If we can demonstrate both of these, then associativity of addition follows by induction.

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎

We have named the proof+-assoc. In Agda, identifiers can consist of any sequence of characters not including spaces or the characters@.(){};_.

Let’s unpack this code. The signature states that we are defining the identifier+-assocwhich provides evidence for the proposition:

∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

The upside down A is pronounced “for all”, and the proposition asserts that for all natural numbersm,n, andpthe equation(m + n) + p ≡ m + (n + p)holds. Evidence for the proposition is a function that accepts three natural numbers, binds them tom,n, andp, and returns evidence for the corresponding instance of the equation.

For the base case, we must show:

(zero + n) + p ≡ zero + (n + p)

Simplifying both sides with the base case of addition yields the equation:

n + p ≡ n + p

This holds trivially. Reading the chain of equations in the base case of the proof, the top and bottom of the chain match the two sides of the equation to be shown, and reading down from the top and up from the bottom takes us ton + pin the middle. No justification other than simplification is required.

For the inductive case, we must show:

(suc m + n) + p ≡ suc m + (n + p)

Simplifying both sides with the inductive case of addition yields the equation:

suc ((m + n) + p) ≡ suc (m + (n + p))

This in turn follows by prefacingsucto both sides of the induction hypothesis:

(m + n) + p ≡ m + (n + p)

Reading the chain of equations in the inductive case of the proof, the top and bottom of the chain match the two sides of the equation to be shown, and reading down from the top and up from the bottom takes us to the simplified equation above. The remaining equation does not follow from simplification alone, so we use an additional operator for chain reasoning,_≡⟨_⟩_, where a justification for the equation appears within angle brackets. The justification given is:

⟨ cong suc (+-assoc m n p) ⟩

Here, the recursive invocation+-assoc m n phas as its type the induction hypothesis, andcong sucprefacessucto each side to yield the needed equation.

A relation is said to be acongruencefor a given function if it is preserved by applying that function. Ifeis evidence thatx ≡ y, thencong f eis evidence thatf x ≡ f y, for any functionf.

Here the inductive hypothesis is not assumed, but instead proved by a recursive invocation of the function we are defining,+-assoc m n p. As with addition, this is well founded because associativity of larger numbers is proved in terms of associativity of smaller numbers. In this case,assoc (suc m) n pis proved usingassoc m n p. The correspondence between proof by induction and definition by recursion is one of the most appealing aspects of Agda.

Induction as recursion

As a concrete example of how induction corresponds to recursion, here is the computation that occurs when instantiatingmto2in the proof of associativity.

+-assoc-2 : ∀ (n p : ℕ) → ( + n) + p ≡  + (n + p)
+-assoc-2 n p =
  begin
    ( + n) + p
  ≡⟨⟩
    suc ( + n) + p
  ≡⟨⟩
    suc (( + n) + p)
  ≡⟨ cong suc (+-assoc-1 n p) ⟩
    suc ( + (n + p))
  ≡⟨⟩
     + (n + p)
  ∎
  where
  +-assoc-1 : ∀ (n p : ℕ) → ( + n) + p ≡  + (n + p)
  +-assoc-1 n p =
    begin
      ( + n) + p
    ≡⟨⟩
      suc ( + n) + p
    ≡⟨⟩
      suc (( + n) + p)
    ≡⟨ cong suc (+-assoc-0 n p) ⟩
      suc ( + (n + p))
    ≡⟨⟩
       + (n + p)
    ∎
    where
    +-assoc-0 : ∀ (n p : ℕ) → ( + n) + p ≡  + (n + p)
    +-assoc-0 n p =
      begin
        ( + n) + p
      ≡⟨⟩
        n + p
      ≡⟨⟩
         + (n + p)
      ∎

Terminology and notation

The symbol∀appears in the statement of associativity to indicate that it holds for all numbersm,n, andp. We refer to∀as theuniversal quantifier, and it is discussed further in ChapterQuantifiers.

Evidence for a universal quantifier is a function. The notations

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

and

+-assoc : ∀ (m : ℕ) → ∀ (n : ℕ) → ∀ (p : ℕ) → (m + n) + p ≡ m + (n + p)

are equivalent. They differ from a function type such asℕ → ℕ → ℕin that variables are associated with each argument type, and the result type may mention (or depend upon) these variables; hence they are calleddependent functions.

Our second proof: commutativity

Another important property of addition is that it iscommutative, that is, that the order of the operands does not matter:

m + n ≡ n + m

The proof requires that we first demonstrate two lemmas.

The first lemma

The base case of the definition of addition states that zero is a left-identity:

zero + n ≡ n

Our first lemma states that zero is also a right-identity:

m + zero ≡ m

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identityʳ (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identityʳ m) ⟩
    suc m
  ∎

The signature states that we are defining the identifier+-identityʳwhich provides evidence for the proposition:

∀ (m : ℕ) → m + zero ≡ m

Evidence for the proposition is a function that accepts a natural number, binds it tom, and returns evidence for the corresponding instance of the equation. The proof is by induction onm.

For the base case, we must show:

zero + zero ≡ zero

Simplifying with the base case of addition, this is straightforward.

For the inductive case, we must show:

(suc m) + zero = suc m

Simplifying both sides with the inductive case of addition yields the equation:

suc (m + zero) = suc m

This in turn follows by prefacingsucto both sides of the induction hypothesis:

m + zero ≡ m

Reading the chain of equations down from the top and up from the bottom takes us to the simplified equation above. The remaining equation has the justification:

⟨ cong suc (+-identityʳ m) ⟩

Here, the recursive invocation+-identityʳ mhas as its type the induction hypothesis, andcong sucprefacessucto each side to yield the needed equation. This completes the first lemma.

The second lemma

The inductive case of the definition of addition pushessucon the first argument to the outside:

suc m + n ≡ suc (m + n)

Our second lemma does the same forsucon the second argument:

m + suc n ≡ suc (m + n)

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

The signature states that we are defining the identifier+-sucwhich provides evidence for the proposition:

∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

Evidence for the proposition is a function that accepts two natural numbers, binds them tomandn, and returns evidence for the corresponding instance of the equation. The proof is by induction onm.

For the base case, we must show:

zero + suc n ≡ suc (zero + n)

Simplifying with the base case of addition, this is straightforward.

For the inductive case, we must show:

suc m + suc n ≡ suc (suc m + n)

Simplifying both sides with the inductive case of addition yields the equation:

suc (m + suc n) ≡ suc (suc (m + n))

This in turn follows by prefacingsucto both sides of the induction hypothesis:

m + suc n ≡ suc (m + n)

Reading the chain of equations down from the top and up from the bottom takes us to the simplified equation in the middle. The remaining equation has the justification:

⟨ cong suc (+-suc m n) ⟩

Here, the recursive invocation+-suc m nhas as its type the induction hypothesis, andcong sucprefacessucto each side to yield the needed equation. This completes the second lemma.

The proposition

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

The first line states that we are defining the identifier+-commwhich provides evidence for the proposition:

∀ (m n : ℕ) → m + n ≡ n + m

Evidence for the proposition is a function that accepts two natural numbers, binds them tomandn, and returns evidence for the corresponding instance of the equation. The proof is by induction onn. (Not onmthis time!)

For the base case, we must show:

m + zero ≡ zero + m

Simplifying both sides with the base case of addition yields the equation:

m + zero ≡ m

The remaining equation has the justification⟨ +-identityʳ m ⟩, which invokes the first lemma.

For the inductive case, we must show:

m + suc n ≡ suc n + m

Simplifying both sides with the inductive case of addition yields the equation:

m + suc n ≡ suc (n + m)

We show this in two steps. First, we have:

m + suc n ≡ suc (m + n)

which is justified by the second lemma,⟨ +-suc m n ⟩. Then we have

suc (m + n) ≡ suc (n + m)

which is justified by congruence and the induction hypothesis,⟨ cong suc (+-comm m n) ⟩. This completes the proof.

Agda requires that identifiers are defined before they are used, so we must present the lemmas before the main proposition, as we have done above. In practice, one will often attempt to prove the main proposition first, and the equations required to do so will suggest what lemmas to prove.

Our first corollary: rearranging

+-rearrange : ∀ (m n p q : ℕ) → (m + n) + (p + q) ≡ m + (n + p) + q
+-rearrange m n p q =
  begin
    (m + n) + (p + q)
  ≡⟨ sym (+-assoc (m + n) p q) ⟩
    ((m + n) + p) + q
  ≡⟨ cong (_+ q) (+-assoc m n p) ⟩
    (m + (n + p)) + q
  ∎

No induction is required, we simply apply associativity twice. A few points are worthy of note.

First, addition associates to the left, som + (n + p) + qstands for(m + (n + p)) + q.

Second, we usesymto interchange the sides of an equation. Proposition+-assoc (m + n) p qshifts parentheses from left to right:

((m + n) + p) + q ≡ (m + n) + (p + q)

To shift them the other way, we usesym (+-assoc n p q):

(m + n) + (p + q) ≡ ((m + n) + p) + q

In general, ifeprovides evidence forx ≡ ythensym eprovides evidence fory ≡ x.

Third, Agda supports a variant of thesectionnotation introduced by Richard Bird. We write(_+ y)for the function that applied toxreturnsx + y. Thus, applying the congruencecong (_+ q)toassoc m n ptakes the equation:

(m + n) + p  ≡  m + (n + p)

into the equation:

((m + n) + p) + q  ≡  (m + (n + p)) + q

Similarly, we write(x +_)for the function that applied toyreturnsx + y; the same works for any infix operator.

Creation, one last time

Returning to the proof of associativity, it may be helpful to view the inductive proof (or, equivalently, the recursive definition) as a creation story. This time we are concerned with judgments asserting associativity:

 -- In the beginning, we know nothing about associativity.

Now, we apply the rules to all the judgments we know about. The base case tells us that(zero + n) + p ≡ zero + (n + p)for every naturalnandp. The inductive case tells us that if(m + n) + p ≡ m + (n + p)(on the day before today) then(suc m + n) + p ≡ suc m + (n + p)(today). We didn’t know any judgments about associativity before today, so that rule doesn’t give us any new judgments:

-- On the first day, we know about associativity of 0.
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...

Then we repeat the process, so on the next day we know about all the judgments from the day before, plus any judgments added by the rules. The base case tells us nothing new, but now the inductive case adds more judgments:

-- On the second day, we know about associativity of 0 and 1.
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...

And we repeat the process again:

-- On the third day, we know about associativity of 0, 1, and 2.
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...
(2 + 0) + 0 ≡ 2 + (0 + 0)   ...   (2 + 4) + 5 ≡ 2 + (4 + 5)   ...

You’ve got the hang of it by now:

-- On the fourth day, we know about associativity of 0, 1, 2, and 3.
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...
(2 + 0) + 0 ≡ 2 + (0 + 0)   ...   (2 + 4) + 5 ≡ 2 + (4 + 5)   ...
(3 + 0) + 0 ≡ 3 + (0 + 0)   ...   (3 + 4) + 5 ≡ 3 + (4 + 5)   ...

The process continues. On them’th day we will know all the judgments where the first number is less thanm.

There is also a completely finite approach to generating the same equations, which is left as an exercise for the reader.

Exercisefinite-+-assoc(stretch)

Write out what is known about associativity of addition on each of the first four days using a finite story of creation, asearlier.

-- Your code goes here

Associativity with rewrite

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero    n p                          =  refl
+-assoc′ (suc m) n p  rewrite +-assoc′ m n p  =  refl

For the base case, we must show:

(zero + n) + p ≡ zero + (n + p)

Simplifying both sides with the base case of addition yields the equation:

n + p ≡ n + p

This holds trivially. The proof that a term is equal to itself is writtenrefl.

For the inductive case, we must show:

(suc m + n) + p ≡ suc m + (n + p)

Simplifying both sides with the inductive case of addition yields the equation:

suc ((m + n) + p) ≡ suc (m + (n + p))

This is our goal to be proved. Rewriting by a given equation is indicated by the keywordrewritefollowed by a proof of that equation. Rewriting replaces each occurrence of the left-hand side of the equation in the goal by the right-hand side. In this case, after rewriting by the inductive hypothesis our goal becomes

suc (m + (n + p)) ≡ suc (m + (n + p))

and the proof is again given byrefl. Rewriting avoids not only chains of equations but also the need to invokecong.

Commutativity with rewrite

+-identity′ : ∀ (n : ℕ) → n + zero ≡ n
+-identity′ zero = refl
+-identity′ (suc n) rewrite +-identity′ n = refl

+-suc′ : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc′ zero n = refl
+-suc′ (suc m) n rewrite +-suc′ m n = refl

+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ m zero rewrite +-identity′ m = refl
+-comm′ m (suc n) rewrite +-suc′ m n | +-comm′ m n = refl

In the final line, rewriting with two equations is indicated by separating the two proofs of the relevant equations by a vertical bar; the rewrite on the left is performed before that on the right.

Building proofs interactively

It is instructive to see how to build the alternative proof of associativity using the interactive features of Agda in Emacs. Begin by typing:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ m n p = ?

The question mark indicates that you would like Agda to help with filling in that part of the code. If you typeC-c C-l(control-c followed by control-l), the question mark will be replaced:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ m n p = { }0

The empty braces are called ahole, and 0 is a number used for referring to the hole. The hole may display highlighted in green. Emacs will also create a new window at the bottom of the screen displaying the text:

?0 : ((m + n) + p) ≡ (m + (n + p))

This indicates that hole 0 is to be filled in with a proof of the stated judgment.

We wish to prove the proposition by induction onm. Move the cursor into the hole and typeC-c C-c. You will be given the prompt:

pattern variables to case (empty for split on result):

Typingmwill cause a split on that variable, resulting in an update to the code:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = { }0
+-assoc′ (suc m) n p = { }1

There are now two holes, and the window at the bottom tells you what each is required to prove:

?0 : ((zero + n) + p) ≡ (zero + (n + p))
?1 : ((suc m + n) + p) ≡ (suc m + (n + p))

Going into hole 0 and typingC-c C-,will display the text:

Goal: (n + p) ≡ (n + p)
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ

This indicates that after simplification the goal for hole 0 is as stated, and that variablespandnof the stated types are available to use in the proof. The proof of the given goal is trivial, and going into the goal and typingC-c C-rwill fill it in. TypingC-c C-lrenumbers the remaining hole to 0:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p = { }0

Going into the new hole 0 and typingC-c C-,will display the text:

Goal: suc ((m + n) + p) ≡ suc (m + (n + p))
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ
m : ℕ

Again, this gives the simplified goal and the available variables. In this case, we need to rewrite by the induction hypothesis, so let’s edit the text accordingly:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = { }0

Going into the remaining hole and typingC-c C-,will display the text:

Goal: suc (m + (n + p)) ≡ suc (m + (n + p))
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ
m : ℕ

The proof of the given goal is trivial, and going into the goal and typingC-c C-rwill fill it in, completing the proof:

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl

Exercise+-swap(recommended)

Show

m + (n + p) ≡ n + (m + p)

for all naturalsm,n, andp. No induction is needed, just apply the previous results which show addition is associative and commutative.

-- Your code goes here

Exercise*-distrib-+(recommended)

Show multiplication distributes over addition, that is,

(m + n) * p ≡ m * p + n * p

for all naturalsm,n, andp.

-- Your code goes here

Exercise*-assoc(recommended)

Show multiplication is associative, that is,

(m * n) * p ≡ m * (n * p)

for all naturalsm,n, andp.

-- Your code goes here

Exercise*-comm(practice)

Show multiplication is commutative, that is,

m * n ≡ n * m

for all naturalsmandn. As with commutativity of addition, you will need to formulate and prove suitable lemmas.

-- Your code goes here

Exercise0∸n≡0(practice)

Show

zero ∸ n ≡ zero

for all naturalsn. Did your proof require induction?

-- Your code goes here

Exercise∸-+-assoc(practice)

Show that monus associates with addition, that is,

m ∸ n ∸ p ≡ m ∸ (n + p)

for all naturalsm,n, andp.

-- Your code goes here

Exercise+*^(stretch)

Show the following three laws

 m ^ (n + p) ≡ (m ^ n) * (m ^ p)  (^-distribˡ-+-*)
 (m * n) ^ p ≡ (m ^ p) * (n ^ p)  (^-distribʳ-*)
 (m ^ n) ^ p ≡ m ^ (n * p)        (^-*-assoc)

for allm,n, andp.

-- Your code goes here

ExerciseBin-laws(stretch)

Recall that ExerciseBindefines a datatypeBinof bitstrings representing natural numbers, and asks you to define functions

inc   : Bin → Bin
to    : ℕ → Bin
from  : Bin → ℕ

Consider the following laws, wherenranges over naturals andbover bitstrings:

from (inc b) ≡ suc (from b)
to (from b) ≡ b
from (to n) ≡ n

For each law: if it holds, prove; if not, give a counterexample.

-- Your code goes here

Standard library

import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)

Unicode

This chapter uses the following unicode:

∀  U+2200  FOR ALL (\forall, \all)
ʳ  U+02B3  MODIFIER LETTER SMALL R (\^r)
′  U+2032  PRIME (\')
″  U+2033  DOUBLE PRIME (\')
‴  U+2034  TRIPLE PRIME (\')
⁗  U+2057  QUADRUPLE PRIME (\')

Similar to\r, the command\^rgives access to a variety of superscript rightward arrows, and also a superscript letterr. The command\'gives access to a range of primes (′ ″ ‴ ⁗).

Relations: Inductive definition of relations

module plfa.part1.Relations where

After having defined operations such as addition and multiplication, the next step is to define relations, such asless than or equal.

Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm; +-identityʳ)

Defining relations

The relationless than or equalhas an infinite number of instances. Here are a few of them:

0 ≤ 0     0 ≤ 1     0 ≤ 2     0 ≤ 3     ...
          1 ≤ 1     1 ≤ 2     1 ≤ 3     ...
                    2 ≤ 2     2 ≤ 3     ...
                              3 ≤ 3     ...
                                        ...

And yet, we can write a finite definition that encompasses all of these instances in just a few lines. Here is the definition as a pair of inference rules:

z≤n --------
    zero ≤ n

    m ≤ n
s≤s -------------
    suc m ≤ suc n

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ}
      --------
    → zero ≤ n

  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      -------------
    → suc m ≤ suc n

Herez≤nands≤s(with no spaces) are constructor names, whilezero ≤ n, andm ≤ nandsuc m ≤ suc n(with spaces) are types. This is our first use of anindexeddatatype, where the typem ≤ nis indexed by two naturals,mandn. In Agda any line beginning with two or more dashes is a comment, and here we have exploited that convention to write our Agda code in a form that resembles the corresponding inference rules, a trick we will use often from now on.

Both definitions above tell us the same two things:

• Base case: for all naturalsn, the propositionzero ≤ nholds.
• Inductive case: for all naturalsmandn, if the propositionm ≤ nholds, then the propositionsuc m ≤ suc nholds.

In fact, they each give us a bit more detail:

• Base case: for all naturalsn, the constructorz≤nproduces evidence thatzero ≤ nholds.
• Inductive case: for all naturalsmandn, the constructors≤stakes evidence thatm ≤ nholds into evidence thatsuc m ≤ suc nholds.

For example, here in inference rule notation is the proof that2 ≤ 4:

  z≤n -----
      0 ≤ 2
 s≤s -------
      1 ≤ 3
s≤s ---------
      2 ≤ 4

_ :  ≤ 
_ = s≤s (s≤s z≤n)

Implicit arguments

This is our first use of implicit arguments. In the definition of inequality, the two lines defining the constructors use∀, very similar to our use of∀in propositions such as:

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m

However, here the declarations are surrounded by curly braces{ }rather than parentheses( ). This means that the arguments areimplicitand need not be written explicitly; instead, they areinferredby Agda’s typechecker. Thus, we write+-comm m nfor the proof thatm + n ≡ n + m, butz≤nfor the proof thatzero ≤ n, leavingnimplicit. Similarly, ifm≤nis evidence thatm ≤ n, we writes≤s m≤nfor evidence thatsuc m ≤ suc n, leaving bothmandnimplicit.

_ :  ≤ 
_ = s≤s {} {} (s≤s {} {} (z≤n {}))

_ :  ≤ 
_ = s≤s {m = } {n = } (s≤s {m = } {n = } (z≤n {n = }))

_ :  ≤ 
_ = s≤s {n = } (s≤s {n = } z≤n)

It is not permitted to swap implicit arguments, even when named.

+-identityʳ′ : ∀ {m : ℕ} → m + zero ≡ m
+-identityʳ′ = +-identityʳ _

We use_to ask Agda to infer the value of theexplicitargument from context. There is only one value which gives us the correct proof,m, so Agda happily fills it in. If Agda fails to infer the value, it reports an error.

Precedence

infix  _≤_

We set the precedence of_≤_at level 4, so it binds less tightly than_+_at level 6 and hence1 + 2 ≤ 3parses as(1 + 2) ≤ 3. We writeinfixto indicate that the operator does not associate to either the left or right, as it makes no sense to parse1 ≤ 2 ≤ 3as either(1 ≤ 2) ≤ 3or1 ≤ (2 ≤ 3).

Decidability

Given two numbers, it is straightforward to compute whether or not the first is less than or equal to the second. We don’t give the code for doing so here, but will return to this point in ChapterDecidable.

Inversion

In our definitions, we go from smaller things to larger things. For instance, fromm ≤ nwe can concludesuc m ≤ suc n, wheresuc mis bigger thanm(that is, the former contains the latter), andsuc nis bigger thann. But sometimes we want to go from bigger things to smaller things.

inv-s≤s : ∀ {m n : ℕ}
  → suc m ≤ suc n
    -------------
  → m ≤ n
inv-s≤s (s≤s m≤n) = m≤n

Herem≤n(with no spaces) is a variable name whilem ≤ n(with spaces) is a type, and the latter is the type of the former. It is a common convention in Agda to derive a variable name by removing spaces from its type.

Not every rule is invertible; indeed, the rule forz≤nhas no non-implicit hypotheses, so there is nothing to invert. But often inversions of this kind hold.

inv-z≤n : ∀ {m : ℕ}
  → m ≤ zero
    --------
  → m ≡ zero
inv-z≤n z≤n = refl

Properties of ordering relations

Relations pop up all the time, and mathematicians have agreed on names for some of the most common properties.

• Reflexive. For alln, the relationn ≤ nholds.
• Transitive. For allm,n, andp, ifm ≤ nandn ≤ phold, thenm ≤ pholds.
• Anti-symmetric. For allmandn, if bothm ≤ nandn ≤ mhold, thenm ≡ nholds.
• Total. For allmandn, eitherm ≤ norn ≤ mholds.

The relation_≤_satisfies all four of these properties.

There are also names for some combinations of these properties.

• Preorder. Any relation that is reflexive and transitive.
• Partial order. Any preorder that is also anti-symmetric.
• Total order. Any partial order that is also total.

If you ever bump into a relation at a party, you now know how to make small talk, by asking it whether it is reflexive, transitive, anti-symmetric, and total. Or instead you might ask whether it is a preorder, partial order, or total order.

Less frivolously, if you ever bump into a relation while reading a technical paper, this gives you a way to orient yourself, by checking whether or not it is a preorder, partial order, or total order. A careful author will often call out these properties—or their lack—for instance by saying that a newly introduced relation is a partial order but not a total order.

Exerciseorderings(practice)

Give an example of a preorder that is not a partial order.

-- Your code goes here

Give an example of a partial order that is not a total order.

-- Your code goes here

Reflexivity

≤-refl : ∀ {n : ℕ}
    -----
  → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl

The proof is a straightforward induction on the implicit argumentn. In the base case,zero ≤ zeroholds byz≤n. In the inductive case, the inductive hypothesis≤-refl {n}gives us a proof ofn ≤ n, and applyings≤sto that yields a proof ofsuc n ≤ suc n.

It is a good exercise to prove reflexivity interactively in Emacs, using holes and theC-c C-c,C-c C-,, andC-c C-rcommands.

Transitivity

≤-trans : ∀ {m n p : ℕ}
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans z≤n       _          =  z≤n
≤-trans (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans m≤n n≤p)

Here the proof is by induction on theevidencethatm ≤ n. In the base case, the first inequality holds byz≤nand must showzero ≤ p, which follows immediately byz≤n. In this case, the fact thatn ≤ pis irrelevant, and we write_as the pattern to indicate that the corresponding evidence is unused.

In the inductive case, the first inequality holds bys≤s m≤nand the second inequality bys≤s n≤p, and so we are givensuc m ≤ suc nandsuc n ≤ suc p, and must showsuc m ≤ suc p. The inductive hypothesis≤-trans m≤n n≤pestablishes thatm ≤ p, and our goal follows by applyings≤s.

The case≤-trans (s≤s m≤n) z≤ncannot arise, since the first inequality implies the middle value issuc nwhile the second inequality implies that it iszero. Agda can determine that such a case cannot arise, and does not require (or permit) it to be listed.

≤-trans′ : ∀ (m n p : ℕ)
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans′ zero    _       _       z≤n       _          =  z≤n
≤-trans′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans′ m n p m≤n n≤p)

One might argue that this is clearer or one might argue that the extra length obscures the essence of the proof. We will usually opt for shorter proofs.

The technique of induction on evidence that a property holds (e.g., inducting on evidence thatm ≤ n)—rather than induction on values of which the property holds (e.g., inducting onm)—will turn out to be immensely valuable, and one that we use often.

Again, it is a good exercise to prove transitivity interactively in Emacs, using holes and theC-c C-c,C-c C-,, andC-c C-rcommands.

Anti-symmetry

≤-antisym : ∀ {m n : ℕ}
  → m ≤ n
  → n ≤ m
    -----
  → m ≡ n
≤-antisym z≤n       z≤n        =  refl
≤-antisym (s≤s m≤n) (s≤s n≤m)  =  cong suc (≤-antisym m≤n n≤m)

Again, the proof is by induction over the evidence thatm ≤ nandn ≤ mhold.

In the base case, both inequalities hold byz≤n, and so we are givenzero ≤ zeroandzero ≤ zeroand must showzero ≡ zero, which follows by reflexivity. (Reflexivity of equality, that is, not reflexivity of inequality.)

In the inductive case, the first inequality holds bys≤s m≤nand the second inequality holds bys≤s n≤m, and so we are givensuc m ≤ suc nandsuc n ≤ suc mand must showsuc m ≡ suc n. The inductive hypothesis≤-antisym m≤n n≤mestablishes thatm ≡ n, and our goal follows by congruence.

Exercise≤-antisym-cases(practice)

The above proof omits cases where one argument isz≤nand one argument iss≤s. Why is it ok to omit them?

-- Your code goes here

Total

The fourth property to prove about comparison is that it is total: for any naturalsmandneitherm ≤ norn ≤ m, or both ifmandnare equal.

data Total (m n : ℕ) : Set where

  forward :
      m ≤ n
      ---------
    → Total m n

  flipped :
      n ≤ m
      ---------
    → Total m n

Evidence thatTotal m nholds is either of the formforward m≤norflipped n≤m, wherem≤nandn≤mare evidence ofm ≤ nandn ≤ mrespectively.

(For those familiar with logic, the above definition could also be written as a disjunction. Disjunctions will be introduced in ChapterConnectives.)

data Total′ : ℕ → ℕ → Set where

  forward′ : ∀ {m n : ℕ}
    → m ≤ n
      ----------
    → Total′ m n

  flipped′ : ∀ {m n : ℕ}
    → n ≤ m
      ----------
    → Total′ m n

Each parameter of the type translates as an implicit parameter of each constructor. Unlike an indexed datatype, where the indexes can vary (as inzero ≤ nandsuc m ≤ suc n), in a parameterised datatype the parameters must always be the same (as inTotal m n). Parameterised declarations are shorter, easier to read, and occasionally aid Agda’s termination checker, so we will use them in preference to indexed types when possible.

≤-total : ∀ (m n : ℕ) → Total m n
≤-total zero    n                         =  forward z≤n
≤-total (suc m) zero                      =  flipped z≤n
≤-total (suc m) (suc n) with ≤-total m n
...                        | forward m≤n  =  forward (s≤s m≤n)
...                        | flipped n≤m  =  flipped (s≤s n≤m)

In this case the proof is by induction over both the first and second arguments. We perform a case analysis:

• First base case: If the first argument iszeroand the second argument isnthen the forward case holds, withz≤nas evidence thatzero ≤ n.

• Second base case: If the first argument issuc mand the second argument iszerothen the flipped case holds, withz≤nas evidence thatzero ≤ suc m.

• Inductive case: If the first argument issuc mand the second argument issuc n, then the inductive hypothesis≤-total m nestablishes one of the following:

  • The forward case of the inductive hypothesis holds withm≤nas evidence thatm ≤ n, from which it follows that the forward case of the proposition holds withs≤s m≤nas evidence thatsuc m ≤ suc n.

  • The flipped case of the inductive hypothesis holds withn≤mas evidence thatn ≤ m, from which it follows that the flipped case of the proposition holds withs≤s n≤mas evidence thatsuc n ≤ suc m.

This is our first use of thewithclause in Agda. The keywordwithis followed by an expression and one or more subsequent lines. Each line begins with an ellipsis (...) and a vertical bar (|), followed by a pattern to be matched against the expression and the right-hand side of the equation.

≤-total′ : ∀ (m n : ℕ) → Total m n
≤-total′ zero    n        =  forward z≤n
≤-total′ (suc m) zero     =  flipped z≤n
≤-total′ (suc m) (suc n)  =  helper (≤-total′ m n)
  where
  helper : Total m n → Total (suc m) (suc n)
  helper (forward m≤n)  =  forward (s≤s m≤n)
  helper (flipped n≤m)  =  flipped (s≤s n≤m)

This is also our first use of awhereclause in Agda. The keywordwhereis followed by one or more definitions, which must be indented. Any variables bound on the left-hand side of the preceding equation (in this case,mandn) are in scope within the nested definition, and any identifiers bound in the nested definition (in this case,helper) are in scope in the right-hand side of the preceding equation.

≤-total″ : ∀ (m n : ℕ) → Total m n
≤-total″ m       zero                      =  flipped z≤n
≤-total″ zero    (suc n)                   =  forward z≤n
≤-total″ (suc m) (suc n) with ≤-total″ m n
...                         | forward m≤n  =  forward (s≤s m≤n)
...                         | flipped n≤m  =  flipped (s≤s n≤m)

It differs from the original code in that it pattern matches on the second argument before the first argument.

Monotonicity

If one bumps into both an operator and an ordering at a party, one may ask if the operator ismonotonicwith regard to the ordering. For example, addition is monotonic with regard to inequality, meaning:

∀ {m n p q : ℕ} → m ≤ n → p ≤ q → m + p ≤ n + q

+-monoʳ-≤ : ∀ (n p q : ℕ)
  → p ≤ q
    -------------
  → n + p ≤ n + q
+-monoʳ-≤ zero    p q p≤q  =  p≤q
+-monoʳ-≤ (suc n) p q p≤q  =  s≤s (+-monoʳ-≤ n p q p≤q)

The proof is by induction on the first argument.

• Base case: The first argument iszeroin which casezero + p ≤ zero + qsimplifies top ≤ q, the evidence for which is given by the argumentp≤q.

• Inductive case: The first argument issuc n, in which casesuc n + p ≤ suc n + qsimplifies tosuc (n + p) ≤ suc (n + q). The inductive hypothesis+-monoʳ-≤ n p q p≤qestablishes thatn + p ≤ n + q, and our goal follows by applyings≤s.

+-monoˡ-≤ : ∀ (m n p : ℕ)
  → m ≤ n
    -------------
  → m + p ≤ n + p
+-monoˡ-≤ m n p m≤n  rewrite +-comm m p | +-comm n p  = +-monoʳ-≤ p m n m≤n

Rewriting by+-comm m pand+-comm n pconvertsm + p ≤ n + pintop + m ≤ p + n, which is proved by invoking+-monoʳ-≤ p m n m≤n.

+-mono-≤ : ∀ (m n p q : ℕ)
  → m ≤ n
  → p ≤ q
    -------------
  → m + p ≤ n + q
+-mono-≤ m n p q m≤n p≤q  =  ≤-trans (+-monoˡ-≤ m n p m≤n) (+-monoʳ-≤ n p q p≤q)

Invoking+-monoˡ-≤ m n p m≤nprovesm + p ≤ n + pand invoking+-monoʳ-≤ n p q p≤qprovesn + p ≤ n + q, and combining these with transitivity provesm + p ≤ n + q, as was to be shown.

Exercise*-mono-≤(stretch)

Show that multiplication is monotonic with regard to inequality.

-- Your code goes here

Strict inequality

infix  _<_

data _<_ : ℕ → ℕ → Set where

  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

  s<s : ∀ {m n : ℕ}
    → m < n
      -------------
    → suc m < suc n

The key difference is that zero is less than the successor of an arbitrary number, but is not less than zero.

Clearly, strict inequality is not reflexive. However it isirreflexivein thatn < nnever holds for any value ofn. Like inequality, strict inequality is transitive. Strict inequality is not total, but satisfies the closely related property oftrichotomy: for anymandn, exactly one ofm < n,m ≡ n, orm > nholds (where we definem > nto hold exactly whenn < m). It is also monotonic with regards to addition and multiplication.

Most of the above are considered in exercises below. Irreflexivity requires negation, as does the fact that the three cases in trichotomy are mutually exclusive, so those points are deferred to ChapterNegation.

It is straightforward to show thatsuc m ≤ nimpliesm < n, and conversely. One can then give an alternative derivation of the properties of strict inequality, such as transitivity, by exploiting the corresponding properties of inequality.

Exercise<-trans(recommended)

Show that strict inequality is transitive. Use a direct proof. (A later exercise exploits the relation between < and ≤.)

-- Your code goes here

Exercisetrichotomy(practice)

Show that strict inequality satisfies a weak version of trichotomy, in the sense that for anymandnthat one of the following holds: *m < n, *m ≡ n, or *m > n.

Definem > nto be the same asn < m. You will need a suitable data declaration, similar to that used for totality. (We will show that the three cases are exclusive after we introducenegation.)

-- Your code goes here

Exercise+-mono-<(practice)

Show that addition is monotonic with respect to strict inequality. As with inequality, some additional definitions may be required.

-- Your code goes here

Exercise≤-iff-<(recommended)

Show thatsuc m ≤ nimpliesm < n, and conversely.

-- Your code goes here

Exercise<-trans-revisited(practice)

Give an alternative proof that strict inequality is transitive, using the relation between strict inequality and inequality and the fact that inequality is transitive.

-- Your code goes here

Even and odd

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  zero :
      ---------
      even zero

  suc  : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where

  suc  : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

A number is even if it is zero or the successor of an odd number, and odd if it is the successor of an even number.

This is our first use of a mutually recursive datatype declaration. Since each identifier must be defined before it is used, we first declare the indexed typesevenandodd(omitting thewherekeyword and the declarations of the constructors) and then declare the constructors (omitting the signaturesℕ → Setwhich were given earlier).

This is also our first use ofoverloadedconstructors, that is, using the same name for constructors of different types. Heresucmeans one of three constructors:

suc : ℕ → ℕ

suc : ∀ {n : ℕ}
  → odd n
    ------------
  → even (suc n)

suc : ∀ {n : ℕ}
  → even n
    -----------
  → odd (suc n)

Similarly,zerorefers to one of two constructors. Due to how it does type inference, Agda does not allow overloading of defined names, but does allow overloading of constructors. It is recommended that one restrict overloading to related meanings, as we have done here, but it is not required.

e+e≡e : ∀ {m n : ℕ}
  → even m
  → even n
    ------------
  → even (m + n)

o+e≡o : ∀ {m n : ℕ}
  → odd m
  → even n
    -----------
  → odd (m + n)

e+e≡e zero     en  =  en
e+e≡e (suc om) en  =  suc (o+e≡o om en)

o+e≡o (suc em) en  =  suc (e+e≡e em en)

Corresponding to the mutually recursive types, we use two mutually recursive functions, one to show that the sum of two even numbers is even, and the other to show that the sum of an odd and an even number is odd.

This is our first use of mutually recursive functions. Since each identifier must be defined before it is used, we first give the signatures for both functions and then the equations that define them.

To show that the sum of two even numbers is even, consider the evidence that the first number is even. If it is because it is zero, then the sum is even because the second number is even. If it is because it is the successor of an odd number, then the result is even because it is the successor of the sum of an odd and an even number, which is odd.

To show that the sum of an odd and even number is odd, consider the evidence that the first number is odd. If it is because it is the successor of an even number, then the result is odd because it is the successor of the sum of two even numbers, which is even.

Exerciseo+o≡e(stretch)

Show that the sum of two odd numbers is even.

-- Your code goes here

ExerciseBin-predicates(stretch)

Recall that ExerciseBindefines a datatypeBinof bitstrings representing natural numbers. Representations are not unique due to leading zeros. Hence, eleven may be represented by both of the following:

⟨⟩ I O I I
⟨⟩ O O I O I I

Define a predicate

Can : Bin → Set

over all bitstrings that holds if the bitstring is canonical, meaning it has no leading zeros; the first representation of eleven above is canonical, and the second is not. To define it, you will need an auxiliary predicate

One : Bin → Set

that holds only if the bistring has a leading one. A bitstring is canonical if it has a leading one (representing a positive number) or if it consists of a single zero (representing zero).

Show that increment preserves canonical bitstrings:

Can b
------------
Can (inc b)

Show that converting a natural to a bitstring always yields a canonical bitstring:

----------
Can (to n)

Show that converting a canonical bitstring to a natural and back is the identity:

Can b
---------------
to (from b) ≡ b

(Hint: For each of these, you may first need to prove related properties ofOne. Also, you may need to prove that ifOne bthen1is less or equal to the result offrom b.)

-- Your code goes here

Standard library

import Data.Nat using (_≤_; z≤n; s≤s)
import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
                                  +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)

In the standard library,≤-totalis formalised in terms of disjunction (which we define in ChapterConnectives), and+-monoʳ-≤,+-monoˡ-≤,+-mono-≤are proved differently than here, and more arguments are implicit.

Unicode

This chapter uses the following unicode:

≤  U+2264  LESS-THAN OR EQUAL TO (\<=, \le)
≥  U+2265  GREATER-THAN OR EQUAL TO (\>=, \ge)
ˡ  U+02E1  MODIFIER LETTER SMALL L (\^l)
ʳ  U+02B3  MODIFIER LETTER SMALL R (\^r)

The commands\^land\^rgive access to a variety of superscript leftward and rightward arrows in addition to superscript letterslandr.

Equality: Equality and equational reasoning

module plfa.part1.Equality where

Much of our reasoning has involved equality. Given two termsMandN, both of typeA, we writeM ≡ Nto assert thatMandNare interchangeable. So far we have treated equality as a primitive, here we show how to define it as an inductive datatype.

Imports

This chapter has no imports. Every chapter in this book, and nearly every module in the Agda standard library, imports equality. Since we define equality here, any import would create a conflict.

Equality

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

In other words, for any typeAand for anyxof typeA, the constructorreflprovides evidence thatx ≡ x. Hence, every value is equal to itself, and we have no other way of showing values equal. The definition features an asymmetry, in that the first argument to_≡_is given by the parameterx : A, while the second is given by an index inA → Set. This follows our policy of using parameters wherever possible. The first argument to_≡_can be a parameter because it doesn’t vary, while the second must be an index, so it can be required to be equal to the first.

infix  _≡_

We set the precedence of_≡_at level 4, the same as_≤_, which means it binds less tightly than any arithmetic operator. It associates neither to left nor right; writingx ≡ y ≡ zis illegal.

Equality is an equivalence relation

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = refl

How does this proof work? The argument tosymhas typex ≡ y, but on the left-hand side of the equation the argument has been instantiated to the patternrefl, which requires thatxandyare the same. Hence, for the right-hand side of the equation we need a term of typex ≡ x, andreflwill do.

It is instructive to developsyminteractively. To start, we supply a variable for the argument on the left, and a hole for the body on the right:

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym e = {! !}

If we go into the hole and typeC-c C-,then Agda reports:

Goal: .y ≡ .x
————————————————————————————————————————————————————————————
e  : .x ≡ .y
.y : .A
.x : .A
.A : Set

If in the hole we typeC-c C-c ethen Agda will instantiateeto all possible constructors, with one equation for each. There is only one possible constructor:

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = {! !}

If we go into the hole again and typeC-c C-,then Agda now reports:

 Goal: .x ≡ .x
 ————————————————————————————————————————————————————————————
 .x : .A
 .A : Set

This is the key step—Agda has worked out thatxandymust be the same to match the patternrefl!

Finally, if we go back into the hole and typeC-c C-rit will instantiate the hole with the one constructor that yields a value of the expected type:

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = refl

This completes the definition as given above.

trans : ∀ {A : Set} {x y z : A}
  → x ≡ y
  → y ≡ z
    -----
  → x ≡ z
trans refl refl  =  refl

Again, a useful exercise is to carry out an interactive development, checking how Agda’s knowledge changes as each of the two arguments is instantiated.

Congruence and substitution

cong : ∀ {A B : Set} (f : A → B) {x y : A}
  → x ≡ y
    ---------
  → f x ≡ f y
cong f refl  =  refl

cong₂ : ∀ {A B C : Set} (f : A → B → C) {u x : A} {v y : B}
  → u ≡ x
  → v ≡ y
    -------------
  → f u v ≡ f x y
cong₂ f refl refl  =  refl

cong-app : ∀ {A B : Set} {f g : A → B}
  → f ≡ g
    ---------------------
  → ∀ (x : A) → f x ≡ g x
cong-app refl x = refl

subst : ∀ {A : Set} {x y : A} (P : A → Set)
  → x ≡ y
    ---------
  → P x → P y
subst P refl px = px

Chains of equations

module ≡-Reasoning {A : Set} where

  infix   begin_
  infixr  _≡⟨⟩_ _≡⟨_⟩_
  infix   _∎

  begin_ : ∀ {x y : A}
    → x ≡ y
      -----
    → x ≡ y
  begin x≡y  =  x≡y

  _≡⟨⟩_ : ∀ (x : A) {y : A}
    → x ≡ y
      -----
    → x ≡ y
  x ≡⟨⟩ x≡y  =  x≡y

  _≡⟨_⟩_ : ∀ (x : A) {y z : A}
    → x ≡ y
    → y ≡ z
      -----
    → x ≡ z
  x ≡⟨ x≡y ⟩ y≡z  =  trans x≡y y≡z

  _∎ : ∀ (x : A)
      -----
    → x ≡ x
  x ∎  =  refl

open ≡-Reasoning

This is our first use of a nested module. It consists of the keywordmodulefollowed by the module name and any parameters, explicit or implicit, the keywordwhere, and the contents of the module indented. Modules may contain any sort of declaration, including other nested modules. Nested modules are similar to the top-level modules that constitute each chapter of this book, save that the body of a top-level module need not be indented. Opening the module makes all of the definitions available in the current environment.

trans′ : ∀ {A : Set} {x y z : A}
  → x ≡ y
  → y ≡ z
    -----
  → x ≡ z
trans′ {A} {x} {y} {z} x≡y y≡z =
  begin
    x
  ≡⟨ x≡y ⟩
    y
  ≡⟨ y≡z ⟩
    z
  ∎

According to the fixity declarations, the body parses as follows:

begin (x ≡⟨ x≡y ⟩ (y ≡⟨ y≡z ⟩ (z ∎)))

The application ofbeginis purely cosmetic, as it simply returns its argument. That argument consists of_≡⟨_⟩_applied tox,x≡y, andy ≡⟨ y≡z ⟩ (z ∎). The first argument is a term,x, while the second and third arguments are both proofs of equations, in particular proofs ofx ≡ yandy ≡ zrespectively, which are combined bytransin the body of_≡⟨_⟩_to yield a proof ofx ≡ z. The proof ofy ≡ zconsists of_≡⟨_⟩_applied toy,y≡z, andz ∎. The first argument is a term,y, while the second and third arguments are both proofs of equations, in particular proofs ofy ≡ zandz ≡ zrespectively, which are combined bytransin the body of_≡⟨_⟩_to yield a proof ofy ≡ z. Finally, the proof ofz ≡ zconsists of_∎applied to the termz, which yieldsrefl. After simplification, the body is equivalent to the term:

trans x≡y (trans y≡z refl)

We could replace any use of a chain of equations by a chain of applications oftrans; the result would be more compact but harder to read. The trick behind∎means that a chain of equalities simplifies to a chain of applications oftransthat ends intrans e refl, whereeis a term that proves some equality, even thoughealone would do.

Exercisetransand≡-Reasoning(practice)

Sadly, we cannot use the definition of trans’ using ≡-Reasoning as the definition for trans. Can you see why? (Hint: look at the definition of_≡⟨_⟩_)

-- Your code goes here

Chains of equations, another example

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero    + n  =  n
(suc m) + n  =  suc (m + n)

postulate
  +-identity : ∀ (m : ℕ) → m + zero ≡ m
  +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

This is our first use of apostulate. A postulate specifies a signature for an identifier but no definition. Here we postulate something proved earlier to save space. Postulates must be used with caution. If we postulate something false then we could use Agda to prove anything whatsoever.

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identity m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

The reasoning here is similar to that in the preceding section. We use_≡⟨⟩_when no justification is required. One can think of_≡⟨⟩_as equivalent to_≡⟨ refl ⟩_.

Agda always treats a term as equivalent to its simplified term. The reason that one can write

  suc (n + m)
≡⟨⟩
  suc n + m

is because Agda treats both terms as the same. This also means that one could instead interchange the lines and write

  suc n + m
≡⟨⟩
  suc (n + m)

and Agda would not object. Agda only checks that the terms separated by≡⟨⟩have the same simplified form; it’s up to us to write them in an order that will make sense to the reader.

Exercise≤-Reasoning(stretch)

The proof of monotonicity from ChapterRelationscan be written in a more readable form by using an analogue of our notation for≡-Reasoning. Define≤-Reasoninganalogously, and use it to write out an alternative proof that addition is monotonic with regard to inequality. Rewrite all of+-monoˡ-≤,+-monoʳ-≤, and+-mono-≤.

-- Your code goes here

Rewriting

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  even-zero : even zero

  even-suc : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where
  odd-suc : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

In the previous section, we proved addition is commutative. Given evidence thateven (m + n)holds, we ought also to be able to take that as evidence thateven (n + m)holds.

{-# BUILTIN EQUALITY _≡_ #-}

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev  rewrite +-comm n m  =  ev

Hereevranges over evidence thateven (m + n)holds, and we show that it also provides evidence thateven (n + m)holds. In general, the keywordrewriteis followed by evidence of an equality, and that equality is used to rewrite the type of the goal and of any variable in scope.

It is instructive to developeven-comminteractively. To start, we supply variables for the arguments on the left, and a hole for the body on the right:

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev = {! !}

If we go into the hole and typeC-c C-,then Agda reports:

Goal: even (n + m)
————————————————————————————————————————————————————————————
ev : even (m + n)
n  : ℕ
m  : ℕ

Now we add the rewrite:

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev rewrite +-comm n m = {! !}

If we go into the hole again and typeC-c C-,then Agda now reports:

Goal: even (m + n)
————————————————————————————————————————————————————————————
ev : even (m + n)
n  : ℕ
m  : ℕ

The arguments have been swapped in the goal. Now it is trivial to see thatevsatisfies the goal, and typingC-c C-ain the hole causes it to be filled withev. The commandC-c C-aperforms an automated search, including checking whether a variable in scope has the same type as the goal.

Multiple rewrites

+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ zero    n  rewrite +-identity n             =  refl
+-comm′ (suc m) n  rewrite +-suc n m | +-comm′ m n  =  refl

This is far more compact. Among other things, whereas the previous proof requiredcong suc (+-comm m n)as the justification to invoke the inductive hypothesis, here it is sufficient to rewrite with+-comm m n, as rewriting automatically takes congruence into account. Although proofs with rewriting are shorter, proofs as chains of equalities are easier to follow, and we will stick with the latter when feasible.

Rewriting expanded

even-comm′ : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm′ m n ev with   m + n  | +-comm m n
...                  | .(n + m) | refl       = ev

In general, one can followwithby any number of expressions, separated by bars, where each following equation has the same number of patterns. We often write expressions and the corresponding patterns so they line up in columns, as above. Here the first column asserts thatm + nandn + mare identical, and the second column justifies that assertion with evidence of the appropriate equality. Note also the use of thedot pattern,.(n + m). A dot pattern consists of a dot followed by an expression, and is used when other information forces the value matched to be equal to the value of the expression in the dot pattern. In this case, the identification ofm + nandn + mis justified by the subsequent matching of+-comm m nagainstrefl. One might think that the first clause is redundant as the information is inherent in the second clause, but in fact Agda is rather picky on this point: omitting the first clause or reversing the order of the clauses will cause Agda to report an error. (Try it and see!)

even-comm″ : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm″ m n  =  subst even (+-comm m n)

Nonetheless, rewrite is a vital part of the Agda toolkit. We will use it sparingly, but it is occasionally essential.

Leibniz equality

The form of asserting equality that we have used is due to Martin-Löf, and was published in 1975. An older form is due to Leibniz, and was published in 1686. Leibniz asserted theidentity of indiscernibles: two objects are equal if and only if they satisfy the same properties. This principle sometimes goes by the name Leibniz’ Law, and is closely related to Spock’s Law, “A difference that makes no difference is no difference”. Here we define Leibniz equality, and show that two terms satisfy Leibniz equality if and only if they satisfy Martin-Löf equality.

Leibniz equality is usually formalised to state thatx ≐ yholds if every propertyPthat holds ofxalso holds ofy. Perhaps surprisingly, this definition is sufficient to also ensure the converse, that every propertyPthat holds ofyalso holds ofx.

_≐_ : ∀ {A : Set} (x y : A) → Set₁
_≐_ {A} x y = ∀ (P : A → Set) → P x → P y

We cannot write the left-hand side of the equation asx ≐ y, and instead we write_≐_ {A} x yto provide access to the implicit parameterAwhich appears on the right-hand side.

This is our first use oflevels. We cannot assignSetthe typeSet, since this would lead to contradictions such as Russell’s Paradox and Girard’s Paradox. Instead, there is a hierarchy of types, whereSet : Set₁,Set₁ : Set₂, and so on. In fact,Setitself is just an abbreviation forSet₀. Since the equation defining_≐_mentionsSeton the right-hand side, the corresponding signature must useSet₁. We say a bit more about levels below.

refl-≐ : ∀ {A : Set} {x : A}
  → x ≐ x
refl-≐ P Px  =  Px

trans-≐ : ∀ {A : Set} {x y z : A}
  → x ≐ y
  → y ≐ z
    -----
  → x ≐ z
trans-≐ x≐y y≐z P Px  =  y≐z P (x≐y P Px)

sym-≐ : ∀ {A : Set} {x y : A}
  → x ≐ y
    -----
  → y ≐ x
sym-≐ {A} {x} {y} x≐y P  =  Qy
  where
    Q : A → Set
    Q z = P z → P x
    Qx : Q x
    Qx = refl-≐ P
    Qy : Q y
    Qy = x≐y Q Qx

Givenx ≐ y, a specificP, we have to construct a proof thatP yimpliesP x. To do so, we instantiate the equality with a predicateQsuch thatQ zholds ifP zimpliesP x. The propertyQ xis trivial by reflexivity, and henceQ yfollows fromx ≐ y. ButQ yis exactly a proof of what we require, thatP yimpliesP x.

≡-implies-≐ : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → x ≐ y
≡-implies-≐ x≡y P  =  subst P x≡y

This direction follows from substitution, which we showed earlier.

≐-implies-≡ : ∀ {A : Set} {x y : A}
  → x ≐ y
    -----
  → x ≡ y
≐-implies-≡ {A} {x} {y} x≐y  =  Qy
  where
    Q : A → Set
    Q z = x ≡ z
    Qx : Q x
    Qx = refl
    Qy : Q y
    Qy = x≐y Q Qx

The proof is similar to that for symmetry of Leibniz equality. We takeQto be the predicate that holds ofzifx ≡ z. ThenQ xis trivial by reflexivity of Martin-Löf equality, and henceQ yfollows fromx ≐ y. ButQ yis exactly a proof of what we require, thatx ≡ y.

(Parts of this section are adapted from≐≃≡: Leibniz Equality is Isomorphic to Martin-Löf Identity, Parametrically, by Andreas Abel, Jesper Cockx, Dominique Devries, Andreas Nuyts, and Philip Wadler, draft, 2017.)

Universe polymorphism

As we have seen, not every type belongs toSet, but instead every type belongs somewhere in the hierarchySet₀,Set₁,Set₂, and so on, whereSetabbreviatesSet₀, andSet₀ : Set₁,Set₁ : Set₂, and so on. The definition of equality given above is fine if we want to compare two values of a type that belongs toSet, but what if we want to compare two values of a type that belongs toSet ℓfor some arbitrary levelℓ?

open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)

We rename constructorszeroandsuctolzeroandlsucto avoid confusion between levels and naturals.

Levels are isomorphic to natural numbers, and have similar constructors:

lzero : Level
lsuc  : Level → Level

The namesSet₀,Set₁,Set₂, and so on, are abbreviations for

Set lzero
Set (lsuc lzero)
Set (lsuc (lsuc lzero))

and so on. There is also an operator

_⊔_ : Level → Level → Level

that given two levels returns the larger of the two.

data _≡′_ {ℓ : Level} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl′ : x ≡′ x

sym′ : ∀ {ℓ : Level} {A : Set ℓ} {x y : A}
  → x ≡′ y
    ------
  → y ≡′ x
sym′ refl′ = refl′

For simplicity, we avoid universe polymorphism in the definitions given in the text, but most definitions in the standard library, including those for equality, are generalised to arbitrary levels as above.

_≐′_ : ∀ {ℓ : Level} {A : Set ℓ} (x y : A) → Set (lsuc ℓ)
_≐′_ {ℓ} {A} x y = ∀ (P : A → Set ℓ) → P x → P y

Before the signature usedSet₁as the type of a term that includesSet, whereas here the signature usesSet (lsuc ℓ)as the type of a term that includesSet ℓ.

_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
  → (B → C) → (A → B) → A → C
(g ∘ f) x  =  g (f x)

Further information on levels can be found in theAgda docs.

Standard library

-- import Relation.Binary.PropositionalEquality as Eq
-- open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
-- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

Here the imports are shown as comments rather than code to avoid collisions, as mentioned in the introduction.

Unicode

This chapter uses the following unicode:

≡  U+2261  IDENTICAL TO (\==, \equiv)
⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)
⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
∎  U+220E  END OF PROOF (\qed)
≐  U+2250  APPROACHES THE LIMIT (\.=)
ℓ  U+2113  SCRIPT SMALL L (\ell)
⊔  U+2294  SQUARE CUP (\lub)
₀  U+2080  SUBSCRIPT ZERO (\_0)
₁  U+2081  SUBSCRIPT ONE (\_1)
₂  U+2082  SUBSCRIPT TWO (\_2)

Isomorphism: Isomorphism and Embedding

module plfa.part1.Isomorphism where

This section introduces isomorphism as a way of asserting that two types are equal, and embedding as a way of asserting that one type is smaller than another. We apply isomorphisms in the next chapter to demonstrate that operations on types such as product and sum satisfy properties akin to associativity, commutativity, and distributivity.

Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong-app)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

Lambda expressions

The chapter begins with a few preliminaries that will be useful here and elsewhere: lambda expressions, function composition, and extensionality.

Lambda expressionsprovide a compact way to define functions without naming them. A term of the form

λ{ P₁ → N₁; ⋯ ; Pₙ → Nₙ }

is equivalent to a functionfdefined by the equations

f P₁ = N₁
⋯
f Pₙ = Nₙ

where thePₙare patterns (left-hand sides of an equation) and theNₙare expressions (right-hand side of an equation).

In the case that there is one equation and the pattern is a variable, we may also use the syntax

λ x → N

or

λ (x : A) → N

both of which are equivalent toλ{x → N}. The latter allows one to specify the domain of the function.

Often using an anonymous lambda expression is more convenient than using a named function: it avoids a lengthy type declaration; and the definition appears exactly where the function is used, so there is no need for the writer to remember to declare it in advance, or for the reader to search for the definition in the code.

Function composition

_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(g ∘ f) x  = g (f x)

_∘′_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
g ∘′ f  =  λ x → g (f x)

Extensionality

Extensionality asserts that the only way to distinguish functions is by applying them; if two functions applied to the same argument always yield the same result, then they are the same function. It is the converse ofcong-app, as introducedearlier.

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

Postulating extensionality does not lead to difficulties, as it is known to be consistent with the theory that underlies Agda.

_+′_ : ℕ → ℕ → ℕ
m +′ zero  = m
m +′ suc n = suc (m +′ n)

same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n
same-app m n rewrite +-comm m n = helper m n
  where
  helper : ∀ (m n : ℕ) → m +′ n ≡ n + m
  helper m zero    = refl
  helper m (suc n) = cong suc (helper m n)

same : _+′_ ≡ _+_
same = extensionality (λ m → extensionality (λ n → same-app m n))

We occasionally need to postulate extensionality in what follows.

postulate
  ∀-extensionality : ∀ {A : Set} {B : A → Set} {f g : ∀(x : A) → B x}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

Here the type offandghas changed fromA → Bto∀ (x : A) → B x, generalising ordinary functions to dependent functions.

Isomorphism

infix  _≃_
record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

Let’s unpack the definition. An isomorphism between setsAandBconsists of four things:

1. A functiontofromAtoB,
2. A functionfromfromBback toA,
3. Evidencefrom∘toasserting thatfromis aleft-inverseforto,
4. Evidenceto∘fromasserting thatfromis aright-inverseforto.

In particular, the third asserts thatfrom ∘ tois the identity, and the fourth thatto ∘ fromis the identity, hence the names. The declarationopen _≃_makes available the namesto,from,from∘to, andto∘from, otherwise we would need to write_≃_.toand so on.

data _≃′_ (A B : Set): Set where
  mk-≃′ : ∀ (to : A → B) →
          ∀ (from : B → A) →
          ∀ (from∘to : (∀ (x : A) → from (to x) ≡ x)) →
          ∀ (to∘from : (∀ (y : B) → to (from y) ≡ y)) →
          A ≃′ B

to′ : ∀ {A B : Set} → (A ≃′ B) → (A → B)
to′ (mk-≃′ f g g∘f f∘g) = f

from′ : ∀ {A B : Set} → (A ≃′ B) → (B → A)
from′ (mk-≃′ f g g∘f f∘g) = g

from∘to′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (x : A) → from′ A≃B (to′ A≃B x) ≡ x)
from∘to′ (mk-≃′ f g g∘f f∘g) = g∘f

to∘from′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (y : B) → to′ A≃B (from′ A≃B y) ≡ y)
to∘from′ (mk-≃′ f g g∘f f∘g) = f∘g

We construct values of the record type with the syntax

record
  { to    = f
  ; from  = g
  ; from∘to = g∘f
  ; to∘from = f∘g
  }

which corresponds to using the constructor of the corresponding inductive type

mk-≃′ f g g∘f f∘g

wheref,g,g∘f, andf∘gare values of suitable types.

Isomorphism is an equivalence

≃-refl : ∀ {A : Set}
    -----
  → A ≃ A
≃-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    ; to∘from = λ{y → refl}
    }

In the above,toandfromare both bound to identity functions, andfrom∘toandto∘fromare both bound to functions that discard their argument and returnrefl. In this case,reflalone is an adequate proof since for the left inverse,from (to x)simplifies tox, and similarly for the right inverse.

≃-sym : ∀ {A B : Set}
  → A ≃ B
    -----
  → B ≃ A
≃-sym A≃B =
  record
    { to      = from A≃B
    ; from    = to   A≃B
    ; from∘to = to∘from A≃B
    ; to∘from = from∘to A≃B
    }

≃-trans : ∀ {A B C : Set}
  → A ≃ B
  → B ≃ C
    -----
  → A ≃ C
≃-trans A≃B B≃C =
  record
    { to       = to   B≃C ∘ to   A≃B
    ; from     = from A≃B ∘ from B≃C
    ; from∘to  = λ{x →
        begin
          (from A≃B ∘ from B≃C) ((to B≃C ∘ to A≃B) x)
        ≡⟨⟩
          from A≃B (from B≃C (to B≃C (to A≃B x)))
        ≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B x)) ⟩
          from A≃B (to A≃B x)
        ≡⟨ from∘to A≃B x ⟩
          x
        ∎}
    ; to∘from = λ{y →
        begin
          (to B≃C ∘ to A≃B) ((from A≃B ∘ from B≃C) y)
        ≡⟨⟩
          to B≃C (to A≃B (from A≃B (from B≃C y)))
        ≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C y)) ⟩
          to B≃C (from B≃C y)
        ≡⟨ to∘from B≃C y ⟩
          y
        ∎}
     }

Equational reasoning for isomorphism

It is straightforward to support a variant of equational reasoning for isomorphism. We essentially copy the previous definition of equality for isomorphism. We omit the form that corresponds to_≡⟨⟩_, since trivial isomorphisms arise far less often than trivial equalities:

module ≃-Reasoning where

  infix   ≃-begin_
  infixr  _≃⟨_⟩_
  infix   _≃-∎

  ≃-begin_ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≃ B
  ≃-begin A≃B = A≃B

  _≃⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≃ B
    → B ≃ C
      -----
    → A ≃ C
  A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C

  _≃-∎ : ∀ (A : Set)
      -----
    → A ≃ A
  A ≃-∎ = ≃-refl

open ≃-Reasoning

Embedding

We also need the notion ofembedding, which is a weakening of isomorphism. While an isomorphism shows that two types are in one-to-one correspondence, an embedding shows that the first type is included in the second; or, equivalently, that there is a many-to-one correspondence between the second type and the first.

infix  _≲_
record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
open _≲_

It is the same as an isomorphism, save that it lacks theto∘fromfield. Hence, we know thatfromis left-inverse toto, but not thatfromis right-inverse toto.

≲-refl : ∀ {A : Set} → A ≲ A
≲-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    }

≲-trans : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
≲-trans A≲B B≲C =
  record
    { to      = λ{x → to   B≲C (to   A≲B x)}
    ; from    = λ{y → from A≲B (from B≲C y)}
    ; from∘to = λ{x →
        begin
          from A≲B (from B≲C (to B≲C (to A≲B x)))
        ≡⟨ cong (from A≲B) (from∘to B≲C (to A≲B x)) ⟩
          from A≲B (to A≲B x)
        ≡⟨ from∘to A≲B x ⟩
          x
        ∎}
     }

≲-antisym : ∀ {A B : Set}
  → (A≲B : A ≲ B)
  → (B≲A : B ≲ A)
  → (to A≲B ≡ from B≲A)
  → (from A≲B ≡ to B≲A)
    -------------------
  → A ≃ B
≲-antisym A≲B B≲A to≡from from≡to =
  record
    { to      = to A≲B
    ; from    = from A≲B
    ; from∘to = from∘to A≲B
    ; to∘from = λ{y →
        begin
          to A≲B (from A≲B y)
        ≡⟨ cong (to A≲B) (cong-app from≡to y) ⟩
          to A≲B (to B≲A y)
        ≡⟨ cong-app to≡from (to B≲A y) ⟩
          from B≲A (to B≲A y)
        ≡⟨ from∘to B≲A y ⟩
          y
        ∎}
    }

The first three components are copied from the embedding, while the last combines the left inverse ofB ≲ Awith the equivalences of thetoandfromcomponents from the two embeddings to obtain the right inverse of the isomorphism.

Equational reasoning for embedding

We can also support tabular reasoning for embedding, analogous to that used for isomorphism:

module ≲-Reasoning where

  infix   ≲-begin_
  infixr  _≲⟨_⟩_
  infix   _≲-∎

  ≲-begin_ : ∀ {A B : Set}
    → A ≲ B
      -----
    → A ≲ B
  ≲-begin A≲B = A≲B

  _≲⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≲ B
    → B ≲ C
      -----
    → A ≲ C
  A ≲⟨ A≲B ⟩ B≲C = ≲-trans A≲B B≲C

  _≲-∎ : ∀ (A : Set)
      -----
    → A ≲ A
  A ≲-∎ = ≲-refl

open ≲-Reasoning

Exercise≃-implies-≲(practice)

postulate
  ≃-implies-≲ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≲ B

-- Your code goes here

Exercise_⇔_(practice)

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A

Show that equivalence is reflexive, symmetric, and transitive.

-- Your code goes here

ExerciseBin-embedding(stretch)

Recall that ExercisesBinandBin-lawsdefine a datatypeBinof bitstrings representing natural numbers, and asks you to define the following functions and predicates:

to : ℕ → Bin
from : Bin → ℕ

which satisfy the following property:

from (to n) ≡ n

-- Your code goes here

Why dotoandfromnot form an isomorphism?

Standard library

import Function using (_∘_)
import Function.Inverse using (_↔_)
import Function.LeftInverse using (_↞_)

The standard library_↔︎_and_↞_correspond to our_≃_and_≲_, respectively, but those in the standard library are less convenient, since they depend on a nested record structure and are parameterised with regard to an arbitrary notion of equivalence.

Unicode

This chapter uses the following unicode:

∘  U+2218  RING OPERATOR (\o, \circ, \comp)
λ  U+03BB  GREEK SMALL LETTER LAMBDA (\lambda, \Gl)
≃  U+2243  ASYMPTOTICALLY EQUAL TO (\~-)
≲  U+2272  LESS-THAN OR EQUIVALENT TO (\<~)
⇔  U+21D4  LEFT RIGHT DOUBLE ARROW (\<=>)

Connectives: Conjunction, disjunction, and implication

module plfa.part1.Connectives where

This chapter introduces the basic logical connectives, by observing a correspondence between connectives of logic and data types, a principle known asPropositions as Types:

• conjunctionisproduct,
• disjunctionissum,
• trueisunit type,
• falseisempty type,
• implicationisfunction space.

Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ)
open import Function using (_∘_)
open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality)
open plfa.part1.Isomorphism.≃-Reasoning

Conjunction is product

data _×_ (A B : Set) : Set where

  ⟨_,_⟩ :
      A
    → B
      -----
    → A × B

Evidence thatA × Bholds is of the form⟨ M , N ⟩, whereMprovides evidence thatAholds andNprovides evidence thatBholds.

proj₁ : ∀ {A B : Set}
  → A × B
    -----
  → A
proj₁ ⟨ x , y ⟩ = x

proj₂ : ∀ {A B : Set}
  → A × B
    -----
  → B
proj₂ ⟨ x , y ⟩ = y

IfLprovides evidence thatA × Bholds, thenproj₁ Lprovides evidence thatAholds, andproj₂ Lprovides evidence thatBholds.

When⟨_,_⟩appears in a term on the right-hand side of an equation we refer to it as aconstructor, and when it appears in a pattern on the left-hand side of an equation we refer to it as adestructor. We may also refer toproj₁andproj₂as destructors, since they play a similar role.

Other terminology refers to⟨_,_⟩asintroducinga conjunction, and toproj₁andproj₂aseliminatinga conjunction; indeed, the former is sometimes given the name×-Iand the latter two the names×-E₁and×-E₂. As we read the rules from top to bottom, introduction and elimination do what they say on the tin: the firstintroducesa formula for the connective, which appears in the conclusion but not in the hypotheses; the secondeliminatesa formula for the connective, which appears in a hypothesis but not in the conclusion. An introduction rule describes under what conditions we say the connective holds—how todefinethe connective. An elimination rule describes what we may conclude when the connective holds—how tousethe connective.¹

η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× ⟨ x , y ⟩ = refl

The pattern matching on the left-hand side is essential, since replacingwby⟨ x , y ⟩allows both sides of the propositional equality to simplify to the same term.

infixr  _×_

Thus,m ≤ n × n ≤ pparses as(m ≤ n) × (n ≤ p).

record _×′_ (A B : Set) : Set where
  constructor ⟨_,_⟩′
  field
    proj₁′ : A
    proj₂′ : B
open _×′_

The record constructionrecord { proj₁′ = M ; proj₂′ = N }corresponds to the term⟨ M , N ⟩whereMis a term of typeAandNis a term of typeB. The constructor declaration allows us to write⟨ M , N ⟩′in place of the record construction.

η-×′ : ∀ {A B : Set} (w : A ×′ B) → ⟨ proj₁′ w , proj₂′ w ⟩′ ≡ w
η-×′ w = refl

It can be very convenient to have η-equalitydefinitionally, and so the standard library defines_×_as a record type. We use the definition from the standard library in later chapters.

data Bool : Set where
  true  : Bool
  false : Bool

data Tri : Set where
  aa : Tri
  bb : Tri
  cc : Tri

Then the typeBool × Trihas six members:

⟨ true  , aa ⟩    ⟨ true  , bb ⟩    ⟨ true ,  cc ⟩
⟨ false , aa ⟩    ⟨ false , bb ⟩    ⟨ false , cc ⟩

×-count : Bool × Tri → ℕ
×-count ⟨ true  , aa ⟩  =  
×-count ⟨ true  , bb ⟩  =  
×-count ⟨ true  , cc ⟩  =  
×-count ⟨ false , aa ⟩  =  
×-count ⟨ false , bb ⟩  =  
×-count ⟨ false , cc ⟩  =  

Product on types also shares a property with product on numbers in that there is a sense in which it is commutative and associative. In particular, product is commutative and associativeup to isomorphism.